Step | Hyp | Ref
| Expression |
1 | | sincn 24198 |
. . . . . . . . . . 11
|
2 | 1 | a1i 11 |
. . . . . . . . . 10
|
3 | | ioosscn 39716 |
. . . . . . . . . . . . 13
|
4 | 3 | a1i 11 |
. . . . . . . . . . . 12
|
5 | | dirkercncflem4.n |
. . . . . . . . . . . . . 14
|
6 | 5 | nncnd 11036 |
. . . . . . . . . . . . 13
|
7 | | 1cnd 10056 |
. . . . . . . . . . . . . 14
|
8 | 7 | halfcld 11277 |
. . . . . . . . . . . . 13
|
9 | 6, 8 | addcld 10059 |
. . . . . . . . . . . 12
|
10 | | ssid 3624 |
. . . . . . . . . . . . 13
|
11 | 10 | a1i 11 |
. . . . . . . . . . . 12
|
12 | 4, 9, 11 | constcncfg 40084 |
. . . . . . . . . . 11
|
13 | 4, 11 | idcncfg 40085 |
. . . . . . . . . . 11
|
14 | 12, 13 | mulcncf 23215 |
. . . . . . . . . 10
|
15 | 2, 14 | cncfmpt1f 22716 |
. . . . . . . . 9
|
16 | | 2cnd 11093 |
. . . . . . . . . . . . . 14
|
17 | | pirp 24213 |
. . . . . . . . . . . . . . . 16
|
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . 15
|
19 | 18 | rpcnd 11874 |
. . . . . . . . . . . . . 14
|
20 | 16, 19 | mulcld 10060 |
. . . . . . . . . . . . 13
|
21 | | ioossre 12235 |
. . . . . . . . . . . . . . . . . 18
|
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
23 | 22 | sselda 3603 |
. . . . . . . . . . . . . . . 16
|
24 | 23 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
25 | 24 | halfcld 11277 |
. . . . . . . . . . . . . 14
|
26 | 25 | sincld 14860 |
. . . . . . . . . . . . 13
|
27 | 20, 26 | mulcld 10060 |
. . . . . . . . . . . 12
|
28 | | 2rp 11837 |
. . . . . . . . . . . . . . . . . 18
|
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
30 | 29 | rpne0d 11877 |
. . . . . . . . . . . . . . . 16
|
31 | 18 | rpne0d 11877 |
. . . . . . . . . . . . . . . 16
|
32 | 16, 19, 30, 31 | mulne0d 10679 |
. . . . . . . . . . . . . . 15
|
33 | 24, 16, 19, 30, 31 | divdiv1d 10832 |
. . . . . . . . . . . . . . . . . 18
|
34 | | dirkercncflem4.c |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
35 | | dirkercncflem4.a |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
36 | 35 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
37 | 34, 36 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
38 | 37 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . . 22
|
39 | | dirkercncflem4.y |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
40 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
41 | | pire 24210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
42 | 40, 41 | remulcli 10054 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
44 | | 0re 10040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
45 | | 2pos 11112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
46 | | pipos 24212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
47 | 40, 41, 45, 46 | mulgt0ii 10170 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
48 | 44, 47 | gtneii 10149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
50 | 39, 43, 49 | redivcld 10853 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
51 | 50 | flcld 12599 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
52 | 51 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
53 | 52 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
54 | 43 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
55 | 53, 54, 49 | divcan4d 10807 |
. . . . . . . . . . . . . . . . . . . . . 22
|
56 | 38, 55 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . 21
|
57 | 56, 51 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . 20
|
58 | 57 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
59 | 52, 43 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . . . 22
|
60 | 37, 59 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . . . . 21
|
61 | 60 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
62 | 29, 18 | rpmulcld 11888 |
. . . . . . . . . . . . . . . . . . . 20
|
63 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
|
64 | 60 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
65 | 64 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
66 | 35 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
67 | 66 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
68 | | dirkercncflem4.b |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
69 | 67, 68 | eqtr4i 2647 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
70 | 69 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
71 | | dirkercncflem4.e |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
72 | 70, 71 | eqtr4i 2647 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
74 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
75 | 52, 74 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
76 | 75, 43 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
77 | 73, 76 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
78 | 77 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
79 | 78 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
80 | | elioo2 12216 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
81 | 65, 79, 80 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
|
82 | 63, 81 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . 21
|
83 | 82 | simp2d 1074 |
. . . . . . . . . . . . . . . . . . . 20
|
84 | 61, 23, 62, 83 | ltdiv1dd 11929 |
. . . . . . . . . . . . . . . . . . 19
|
85 | 77 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
86 | 82 | simp3d 1075 |
. . . . . . . . . . . . . . . . . . . . 21
|
87 | 23, 85, 62, 86 | ltdiv1dd 11929 |
. . . . . . . . . . . . . . . . . . . 20
|
88 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
89 | 88 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
90 | 89 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . 22
|
91 | 35, 53 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
92 | 91, 54, 49 | divcan4d 10807 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
93 | 92 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . 22
|
94 | 68 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
95 | 71, 94 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
96 | 95 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
97 | 96 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
98 | 91, 7 | addcld 10059 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
99 | 98, 54, 49 | divcan4d 10807 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
100 | 97, 99 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . . . 22
|
101 | 90, 93, 100 | 3eqtrrd 2661 |
. . . . . . . . . . . . . . . . . . . . 21
|
102 | 101 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
103 | 87, 102 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . 19
|
104 | | btwnnz 11453 |
. . . . . . . . . . . . . . . . . . 19
|
105 | 58, 84, 103, 104 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
|
106 | 33, 105 | eqneltrd 2720 |
. . . . . . . . . . . . . . . . 17
|
107 | | sineq0 24273 |
. . . . . . . . . . . . . . . . . 18
|
108 | 25, 107 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
109 | 106, 108 | mtbird 315 |
. . . . . . . . . . . . . . . 16
|
110 | 109 | neqned 2801 |
. . . . . . . . . . . . . . 15
|
111 | 20, 26, 32, 110 | mulne0d 10679 |
. . . . . . . . . . . . . 14
|
112 | 111 | neneqd 2799 |
. . . . . . . . . . . . 13
|
113 | 40 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
114 | 41 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
115 | 113, 114 | remulcld 10070 |
. . . . . . . . . . . . . . 15
|
116 | 23 | rehalfcld 11279 |
. . . . . . . . . . . . . . . 16
|
117 | 116 | resincld 14873 |
. . . . . . . . . . . . . . 15
|
118 | 115, 117 | remulcld 10070 |
. . . . . . . . . . . . . 14
|
119 | | elsng 4191 |
. . . . . . . . . . . . . 14
|
120 | 118, 119 | syl 17 |
. . . . . . . . . . . . 13
|
121 | 112, 120 | mtbird 315 |
. . . . . . . . . . . 12
|
122 | 27, 121 | eldifd 3585 |
. . . . . . . . . . 11
|
123 | | eqidd 2623 |
. . . . . . . . . . 11
|
124 | | eqidd 2623 |
. . . . . . . . . . 11
|
125 | | oveq2 6658 |
. . . . . . . . . . 11
|
126 | 122, 123,
124, 125 | fmptco 6396 |
. . . . . . . . . 10
|
127 | | eqid 2622 |
. . . . . . . . . . . 12
|
128 | | 2cnd 11093 |
. . . . . . . . . . . . . . 15
|
129 | 4, 128, 11 | constcncfg 40084 |
. . . . . . . . . . . . . 14
|
130 | 17 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
131 | 130 | rpcnd 11874 |
. . . . . . . . . . . . . . 15
|
132 | 4, 131, 11 | constcncfg 40084 |
. . . . . . . . . . . . . 14
|
133 | 129, 132 | mulcncf 23215 |
. . . . . . . . . . . . 13
|
134 | 24, 16, 30 | divrecd 10804 |
. . . . . . . . . . . . . . . 16
|
135 | 134 | mpteq2dva 4744 |
. . . . . . . . . . . . . . 15
|
136 | 4, 8, 11 | constcncfg 40084 |
. . . . . . . . . . . . . . . 16
|
137 | 13, 136 | mulcncf 23215 |
. . . . . . . . . . . . . . 15
|
138 | 135, 137 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
|
139 | 2, 138 | cncfmpt1f 22716 |
. . . . . . . . . . . . 13
|
140 | 133, 139 | mulcncf 23215 |
. . . . . . . . . . . 12
|
141 | | ssid 3624 |
. . . . . . . . . . . . 13
|
142 | 141 | a1i 11 |
. . . . . . . . . . . 12
|
143 | | difssd 3738 |
. . . . . . . . . . . 12
|
144 | 127, 140,
142, 143, 122 | cncfmptssg 40083 |
. . . . . . . . . . 11
|
145 | | ax-1cn 9994 |
. . . . . . . . . . . 12
|
146 | | eqid 2622 |
. . . . . . . . . . . . 13
|
147 | 146 | cdivcncf 22720 |
. . . . . . . . . . . 12
|
148 | 145, 147 | mp1i 13 |
. . . . . . . . . . 11
|
149 | 144, 148 | cncfco 22710 |
. . . . . . . . . 10
|
150 | 126, 149 | eqeltrrd 2702 |
. . . . . . . . 9
|
151 | 15, 150 | mulcncf 23215 |
. . . . . . . 8
|
152 | | dirkercncflem4.d |
. . . . . . . . . . . 12
|
153 | 152 | dirkerval 40308 |
. . . . . . . . . . 11
|
154 | 5, 153 | syl 17 |
. . . . . . . . . 10
|
155 | 154 | reseq1d 5395 |
. . . . . . . . 9
|
156 | 22 | resmptd 5452 |
. . . . . . . . 9
|
157 | 28 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
158 | 157, 130 | rpmulcld 11888 |
. . . . . . . . . . . . . . 15
|
159 | 158 | adantr 481 |
. . . . . . . . . . . . . 14
|
160 | | mod0 12675 |
. . . . . . . . . . . . . 14
|
161 | 23, 159, 160 | syl2anc 693 |
. . . . . . . . . . . . 13
|
162 | 105, 161 | mtbird 315 |
. . . . . . . . . . . 12
|
163 | 162 | iffalsed 4097 |
. . . . . . . . . . 11
|
164 | 6 | adantr 481 |
. . . . . . . . . . . . . . 15
|
165 | | 1cnd 10056 |
. . . . . . . . . . . . . . . 16
|
166 | 165 | halfcld 11277 |
. . . . . . . . . . . . . . 15
|
167 | 164, 166 | addcld 10059 |
. . . . . . . . . . . . . 14
|
168 | 167, 24 | mulcld 10060 |
. . . . . . . . . . . . 13
|
169 | 168 | sincld 14860 |
. . . . . . . . . . . 12
|
170 | 169, 27, 111 | divrecd 10804 |
. . . . . . . . . . 11
|
171 | 163, 170 | eqtrd 2656 |
. . . . . . . . . 10
|
172 | 171 | mpteq2dva 4744 |
. . . . . . . . 9
|
173 | 155, 156,
172 | 3eqtrrd 2661 |
. . . . . . . 8
|
174 | | eqid 2622 |
. . . . . . . . . 10
ℂfld ℂfld |
175 | 174 | tgioo2 22606 |
. . . . . . . . . . . 12
ℂfld
↾t |
176 | 175 | oveq1i 6660 |
. . . . . . . . . . 11
↾t ℂfld ↾t
↾t |
177 | 174 | cnfldtop 22587 |
. . . . . . . . . . . 12
ℂfld |
178 | | reex 10027 |
. . . . . . . . . . . 12
|
179 | | restabs 20969 |
. . . . . . . . . . . 12
ℂfld
ℂfld
↾t
↾t ℂfld
↾t |
180 | 177, 21, 178, 179 | mp3an 1424 |
. . . . . . . . . . 11
ℂfld
↾t
↾t ℂfld
↾t |
181 | 176, 180 | eqtri 2644 |
. . . . . . . . . 10
↾t ℂfld ↾t |
182 | | unicntop 22589 |
. . . . . . . . . . . . 13
ℂfld |
183 | 182 | restid 16094 |
. . . . . . . . . . . 12
ℂfld ℂfld
↾t ℂfld |
184 | 177, 183 | ax-mp 5 |
. . . . . . . . . . 11
ℂfld ↾t ℂfld |
185 | 184 | eqcomi 2631 |
. . . . . . . . . 10
ℂfld ℂfld ↾t |
186 | 174, 181,
185 | cncfcn 22712 |
. . . . . . . . 9
↾t ℂfld |
187 | 4, 11, 186 | syl2anc 693 |
. . . . . . . 8
↾t ℂfld |
188 | 151, 173,
187 | 3eltr3d 2715 |
. . . . . . 7
↾t ℂfld |
189 | | retopon 22567 |
. . . . . . . . . 10
TopOn |
190 | 189 | a1i 11 |
. . . . . . . . 9
TopOn |
191 | | resttopon 20965 |
. . . . . . . . 9
TopOn
↾t TopOn |
192 | 190, 22, 191 | syl2anc 693 |
. . . . . . . 8
↾t TopOn |
193 | 174 | cnfldtopon 22586 |
. . . . . . . . 9
ℂfld TopOn |
194 | 193 | a1i 11 |
. . . . . . . 8
ℂfld
TopOn |
195 | | cncnp 21084 |
. . . . . . . 8
↾t TopOn ℂfld TopOn ↾t ℂfld
↾t ℂfld |
196 | 192, 194,
195 | syl2anc 693 |
. . . . . . 7
↾t ℂfld
↾t ℂfld |
197 | 188, 196 | mpbid 222 |
. . . . . 6
↾t ℂfld |
198 | 197 | simprd 479 |
. . . . 5
↾t ℂfld |
199 | | dirkercncflem4.ymod0 |
. . . . . . . . . . . 12
|
200 | 199 | neneqd 2799 |
. . . . . . . . . . 11
|
201 | | mod0 12675 |
. . . . . . . . . . . 12
|
202 | 39, 158, 201 | syl2anc 693 |
. . . . . . . . . . 11
|
203 | 200, 202 | mtbid 314 |
. . . . . . . . . 10
|
204 | | flltnz 12612 |
. . . . . . . . . 10
|
205 | 50, 203, 204 | syl2anc 693 |
. . . . . . . . 9
|
206 | 52, 50, 158, 205 | ltmul1dd 11927 |
. . . . . . . 8
|
207 | 39 | recnd 10068 |
. . . . . . . . 9
|
208 | 207, 54, 49 | divcan1d 10802 |
. . . . . . . 8
|
209 | 206, 208 | breqtrd 4679 |
. . . . . . 7
|
210 | 37, 209 | syl5eqbr 4688 |
. . . . . 6
|
211 | | fllelt 12598 |
. . . . . . . . . 10
|
212 | 50, 211 | syl 17 |
. . . . . . . . 9
|
213 | 212 | simprd 479 |
. . . . . . . 8
|
214 | 50, 75, 158, 213 | ltmul1dd 11927 |
. . . . . . 7
|
215 | 214, 208,
73 | 3brtr3d 4684 |
. . . . . 6
|
216 | 64, 78, 39, 210, 215 | eliood 39720 |
. . . . 5
|
217 | | fveq2 6191 |
. . . . . . 7
↾t ℂfld ↾t ℂfld |
218 | 217 | eleq2d 2687 |
. . . . . 6
↾t ℂfld ↾t ℂfld |
219 | 218 | rspccva 3308 |
. . . . 5
↾t ℂfld
↾t ℂfld |
220 | 198, 216,
219 | syl2anc 693 |
. . . 4
↾t ℂfld |
221 | 177 | a1i 11 |
. . . . 5
ℂfld
|
222 | 152 | dirkerf 40314 |
. . . . . . 7
|
223 | 5, 222 | syl 17 |
. . . . . 6
|
224 | 223, 22 | fssresd 6071 |
. . . . 5
|
225 | | ax-resscn 9993 |
. . . . . 6
|
226 | 225 | a1i 11 |
. . . . 5
|
227 | | retop 22565 |
. . . . . . 7
|
228 | | uniretop 22566 |
. . . . . . . 8
|
229 | 228 | restuni 20966 |
. . . . . . 7
↾t |
230 | 227, 21, 229 | mp2an 708 |
. . . . . 6
↾t |
231 | 230, 182 | cnprest2 21094 |
. . . . 5
ℂfld
↾t ℂfld ↾t ℂfld
↾t |
232 | 221, 224,
226, 231 | syl3anc 1326 |
. . . 4
↾t ℂfld ↾t ℂfld
↾t |
233 | 220, 232 | mpbid 222 |
. . 3
↾t ℂfld ↾t |
234 | 175 | eqcomi 2631 |
. . . . . 6
ℂfld ↾t |
235 | 234 | a1i 11 |
. . . . 5
ℂfld
↾t |
236 | 235 | oveq2d 6666 |
. . . 4
↾t ℂfld
↾t
↾t |
237 | 236 | fveq1d 6193 |
. . 3
↾t ℂfld ↾t ↾t
|
238 | 233, 237 | eleqtrd 2703 |
. 2
↾t |
239 | 227 | a1i 11 |
. . 3
|
240 | | iooretop 22569 |
. . . . . . 7
|
241 | 228 | isopn3 20870 |
. . . . . . 7
|
242 | 240, 241 | mpbii 223 |
. . . . . 6
|
243 | 239, 22, 242 | syl2anc 693 |
. . . . 5
|
244 | 243 | eqcomd 2628 |
. . . 4
|
245 | 216, 244 | eleqtrd 2703 |
. . 3
|
246 | 228, 228 | cnprest 21093 |
. . 3
↾t |
247 | 239, 22, 245, 223, 246 | syl22anc 1327 |
. 2
↾t |
248 | 238, 247 | mpbird 247 |
1
|