Step | Hyp | Ref
| Expression |
1 | | rge0ssre 12280 |
. . . . . . . 8
|
2 | | ax-resscn 9993 |
. . . . . . . 8
|
3 | 1, 2 | sstri 3612 |
. . . . . . 7
|
4 | 3 | sseli 3599 |
. . . . . 6
|
5 | | simpll 790 |
. . . . . . . . . . 11
|
6 | | 1cnd 10056 |
. . . . . . . . . . 11
|
7 | | simplr 792 |
. . . . . . . . . . 11
|
8 | | ax-1ne0 10005 |
. . . . . . . . . . . 12
|
9 | 8 | a1i 11 |
. . . . . . . . . . 11
|
10 | | simpr 477 |
. . . . . . . . . . . 12
|
11 | 10 | neqned 2801 |
. . . . . . . . . . 11
|
12 | 5, 6, 7, 9, 11 | divdiv2d 10833 |
. . . . . . . . . 10
|
13 | | mulcl 10020 |
. . . . . . . . . . . 12
|
14 | 13 | adantr 481 |
. . . . . . . . . . 11
|
15 | 14 | div1d 10793 |
. . . . . . . . . 10
|
16 | 12, 15 | eqtrd 2656 |
. . . . . . . . 9
|
17 | 16 | oveq2d 6666 |
. . . . . . . 8
|
18 | 17 | oveq1d 6665 |
. . . . . . 7
|
19 | 18 | ifeq2da 4117 |
. . . . . 6
|
20 | 4, 19 | sylan2 491 |
. . . . 5
|
21 | 20 | mpteq2dva 4744 |
. . . 4
|
22 | | resmpt 5449 |
. . . . 5
|
23 | 3, 22 | ax-mp 5 |
. . . 4
|
24 | 21, 23 | syl6eqr 2674 |
. . 3
|
25 | 3 | a1i 11 |
. . . 4
|
26 | | 0e0icopnf 12282 |
. . . . 5
|
27 | 26 | a1i 11 |
. . . 4
|
28 | | eqeq2 2633 |
. . . . . . . . 9
|
29 | | eqeq2 2633 |
. . . . . . . . 9
|
30 | | efrlim.1 |
. . . . . . . . . . . . . 14
|
31 | | cnxmet 22576 |
. . . . . . . . . . . . . . . 16
|
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . 15
|
33 | | 0cnd 10033 |
. . . . . . . . . . . . . . 15
|
34 | | abscl 14018 |
. . . . . . . . . . . . . . . . . . 19
|
35 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . 19
|
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
37 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . 19
|
38 | | absge0 14027 |
. . . . . . . . . . . . . . . . . . 19
|
39 | 34 | ltp1d 10954 |
. . . . . . . . . . . . . . . . . . 19
|
40 | 37, 34, 36, 38, 39 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . 18
|
41 | 36, 40 | elrpd 11869 |
. . . . . . . . . . . . . . . . 17
|
42 | 41 | rpreccld 11882 |
. . . . . . . . . . . . . . . 16
|
43 | 42 | rpxrd 11873 |
. . . . . . . . . . . . . . 15
|
44 | | blssm 22223 |
. . . . . . . . . . . . . . 15
|
45 | 32, 33, 43, 44 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
46 | 30, 45 | syl5eqss 3649 |
. . . . . . . . . . . . 13
|
47 | 46 | sselda 3603 |
. . . . . . . . . . . 12
|
48 | | mul0or 10667 |
. . . . . . . . . . . 12
|
49 | 47, 48 | syldan 487 |
. . . . . . . . . . 11
|
50 | 49 | biimpa 501 |
. . . . . . . . . 10
|
51 | | simpl 473 |
. . . . . . . . . . . . . . . . . . 19
|
52 | 51, 47 | jca 554 |
. . . . . . . . . . . . . . . . . 18
|
53 | 7, 11 | reccld 10794 |
. . . . . . . . . . . . . . . . . 18
|
54 | 52, 53 | sylan 488 |
. . . . . . . . . . . . . . . . 17
|
55 | 54 | adantlr 751 |
. . . . . . . . . . . . . . . 16
|
56 | 55 | 1cxpd 24453 |
. . . . . . . . . . . . . . 15
|
57 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . 20
|
58 | 57 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
|
59 | 47 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
|
60 | 59 | mul02d 10234 |
. . . . . . . . . . . . . . . . . . 19
|
61 | 58, 60 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
|
62 | 61 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
63 | | 1p0e1 11133 |
. . . . . . . . . . . . . . . . 17
|
64 | 62, 63 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
|
65 | 64 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
66 | 57 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
67 | | ef0 14821 |
. . . . . . . . . . . . . . . 16
|
68 | 66, 67 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
|
69 | 56, 65, 68 | 3eqtr4d 2666 |
. . . . . . . . . . . . . 14
|
70 | 69 | ifeq2da 4117 |
. . . . . . . . . . . . 13
|
71 | | ifid 4125 |
. . . . . . . . . . . . 13
|
72 | 70, 71 | syl6eq 2672 |
. . . . . . . . . . . 12
|
73 | | iftrue 4092 |
. . . . . . . . . . . . 13
|
74 | 73 | adantl 482 |
. . . . . . . . . . . 12
|
75 | 72, 74 | jaodan 826 |
. . . . . . . . . . 11
|
76 | | mulid1 10037 |
. . . . . . . . . . . . 13
|
77 | 76 | ad2antrr 762 |
. . . . . . . . . . . 12
|
78 | 77 | fveq2d 6195 |
. . . . . . . . . . 11
|
79 | 75, 78 | eqtr4d 2659 |
. . . . . . . . . 10
|
80 | 50, 79 | syldan 487 |
. . . . . . . . 9
|
81 | | mulne0b 10668 |
. . . . . . . . . . . . 13
|
82 | 47, 81 | syldan 487 |
. . . . . . . . . . . 12
|
83 | | df-ne 2795 |
. . . . . . . . . . . 12
|
84 | 82, 83 | syl6bb 276 |
. . . . . . . . . . 11
|
85 | | simprr 796 |
. . . . . . . . . . . . . . 15
|
86 | 85 | neneqd 2799 |
. . . . . . . . . . . . . 14
|
87 | 86 | iffalsed 4097 |
. . . . . . . . . . . . 13
|
88 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . 16
|
89 | 47, 13 | syldan 487 |
. . . . . . . . . . . . . . . 16
|
90 | | addcl 10018 |
. . . . . . . . . . . . . . . 16
|
91 | 88, 89, 90 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
92 | 91 | adantr 481 |
. . . . . . . . . . . . . 14
|
93 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
|
94 | 93 | dvlog2lem 24398 |
. . . . . . . . . . . . . . . . . 18
|
95 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
|
96 | 95 | logdmss 24388 |
. . . . . . . . . . . . . . . . . 18
|
97 | 94, 96 | sstri 3612 |
. . . . . . . . . . . . . . . . 17
|
98 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
|
99 | 98 | cnmetdval 22574 |
. . . . . . . . . . . . . . . . . . . . 21
|
100 | 91, 88, 99 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . 20
|
101 | | pncan2 10288 |
. . . . . . . . . . . . . . . . . . . . . 22
|
102 | 88, 89, 101 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . 21
|
103 | 102 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
104 | 100, 103 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
|
105 | 89 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . 20
|
106 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
107 | 47 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . 21
|
108 | 106, 107 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . 20
|
109 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . 20
|
110 | | absmul 14034 |
. . . . . . . . . . . . . . . . . . . . . 22
|
111 | 47, 110 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . 21
|
112 | 34 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
113 | 112, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
114 | 47 | absge0d 14183 |
. . . . . . . . . . . . . . . . . . . . . 22
|
115 | 112 | lep1d 10955 |
. . . . . . . . . . . . . . . . . . . . . 22
|
116 | 112, 113,
107, 114, 115 | lemul1ad 10963 |
. . . . . . . . . . . . . . . . . . . . 21
|
117 | 111, 116 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . . 20
|
118 | | 0cn 10032 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
119 | 98 | cnmetdval 22574 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
120 | 47, 118, 119 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
121 | 47 | subid1d 10381 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
122 | 121 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
123 | 120, 122 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
|
124 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
125 | 124, 30 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
126 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
127 | 43 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
128 | | 0cnd 10033 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
129 | | elbl3 22197 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
130 | 126, 127,
128, 47, 129 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
131 | 125, 130 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . 22
|
132 | 123, 131 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . . . . . 21
|
133 | 40 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
134 | | ltmuldiv2 10897 |
. . . . . . . . . . . . . . . . . . . . . 22
|
135 | 107, 109,
113, 133, 134 | syl112anc 1330 |
. . . . . . . . . . . . . . . . . . . . 21
|
136 | 132, 135 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . 20
|
137 | 105, 108,
109, 117, 136 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . 19
|
138 | 104, 137 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . 18
|
139 | | 1rp 11836 |
. . . . . . . . . . . . . . . . . . . 20
|
140 | | rpxr 11840 |
. . . . . . . . . . . . . . . . . . . 20
|
141 | 139, 140 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
|
142 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . 19
|
143 | | elbl3 22197 |
. . . . . . . . . . . . . . . . . . 19
|
144 | 126, 141,
142, 91, 143 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . 18
|
145 | 138, 144 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
|
146 | 97, 145 | sseldi 3601 |
. . . . . . . . . . . . . . . 16
|
147 | | eldifsni 4320 |
. . . . . . . . . . . . . . . 16
|
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . 15
|
149 | 148 | adantr 481 |
. . . . . . . . . . . . . 14
|
150 | 47 | adantr 481 |
. . . . . . . . . . . . . . 15
|
151 | 150, 85 | reccld 10794 |
. . . . . . . . . . . . . 14
|
152 | 92, 149, 151 | cxpefd 24458 |
. . . . . . . . . . . . 13
|
153 | 91, 148 | logcld 24317 |
. . . . . . . . . . . . . . . . 17
|
154 | 153 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
155 | 151, 154 | mulcomd 10061 |
. . . . . . . . . . . . . . 15
|
156 | | simpll 790 |
. . . . . . . . . . . . . . . . . . 19
|
157 | | simprl 794 |
. . . . . . . . . . . . . . . . . . 19
|
158 | 156, 157 | dividd 10799 |
. . . . . . . . . . . . . . . . . 18
|
159 | 158 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
|
160 | 156, 156,
150, 157, 85 | divdiv1d 10832 |
. . . . . . . . . . . . . . . . 17
|
161 | 159, 160 | eqtr3d 2658 |
. . . . . . . . . . . . . . . 16
|
162 | 161 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
163 | 89 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
164 | 82 | biimpa 501 |
. . . . . . . . . . . . . . . 16
|
165 | 154, 156,
163, 164 | div12d 10837 |
. . . . . . . . . . . . . . 15
|
166 | 155, 162,
165 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
|
167 | 166 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
168 | 87, 152, 167 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
169 | 168 | ex 450 |
. . . . . . . . . . 11
|
170 | 84, 169 | sylbird 250 |
. . . . . . . . . 10
|
171 | 170 | imp 445 |
. . . . . . . . 9
|
172 | 28, 29, 80, 171 | ifbothda 4123 |
. . . . . . . 8
|
173 | 172 | mpteq2dva 4744 |
. . . . . . 7
|
174 | 46 | resmptd 5452 |
. . . . . . 7
|
175 | | 1cnd 10056 |
. . . . . . . . 9
|
176 | 153 | adantr 481 |
. . . . . . . . . 10
|
177 | 89 | adantr 481 |
. . . . . . . . . 10
|
178 | | simpr 477 |
. . . . . . . . . . 11
|
179 | 178 | neqned 2801 |
. . . . . . . . . 10
|
180 | 176, 177,
179 | divcld 10801 |
. . . . . . . . 9
|
181 | 175, 180 | ifclda 4120 |
. . . . . . . 8
|
182 | | eqidd 2623 |
. . . . . . . 8
|
183 | | eqidd 2623 |
. . . . . . . 8
|
184 | | oveq2 6658 |
. . . . . . . . . 10
|
185 | 184 | fveq2d 6195 |
. . . . . . . . 9
|
186 | | oveq2 6658 |
. . . . . . . . . . 11
|
187 | 186 | fveq2d 6195 |
. . . . . . . . . 10
|
188 | | oveq2 6658 |
. . . . . . . . . . 11
|
189 | 188 | fveq2d 6195 |
. . . . . . . . . 10
|
190 | 187, 189 | ifsb 4099 |
. . . . . . . . 9
|
191 | 185, 190 | syl6eq 2672 |
. . . . . . . 8
|
192 | 181, 182,
183, 191 | fmptco 6396 |
. . . . . . 7
|
193 | 173, 174,
192 | 3eqtr4d 2666 |
. . . . . 6
|
194 | | eqidd 2623 |
. . . . . . . . . 10
|
195 | | eqidd 2623 |
. . . . . . . . . 10
|
196 | | eqeq1 2626 |
. . . . . . . . . . 11
|
197 | | fveq2 6191 |
. . . . . . . . . . . 12
|
198 | | oveq1 6657 |
. . . . . . . . . . . 12
|
199 | 197, 198 | oveq12d 6668 |
. . . . . . . . . . 11
|
200 | 196, 199 | ifbieq2d 4111 |
. . . . . . . . . 10
|
201 | 145, 194,
195, 200 | fmptco 6396 |
. . . . . . . . 9
|
202 | 63 | eqeq2i 2634 |
. . . . . . . . . . . 12
|
203 | 142, 89, 128 | addcand 10239 |
. . . . . . . . . . . 12
|
204 | 202, 203 | syl5bbr 274 |
. . . . . . . . . . 11
|
205 | 102 | oveq2d 6666 |
. . . . . . . . . . 11
|
206 | 204, 205 | ifbieq2d 4111 |
. . . . . . . . . 10
|
207 | 206 | mpteq2dva 4744 |
. . . . . . . . 9
|
208 | 201, 207 | eqtrd 2656 |
. . . . . . . 8
|
209 | | eqid 2622 |
. . . . . . . . . . . 12
ℂfld ↾t ℂfld
↾t |
210 | | eqid 2622 |
. . . . . . . . . . . . . 14
ℂfld ℂfld |
211 | 210 | cnfldtopon 22586 |
. . . . . . . . . . . . 13
ℂfld TopOn |
212 | 211 | a1i 11 |
. . . . . . . . . . . 12
ℂfld TopOn |
213 | | 1cnd 10056 |
. . . . . . . . . . . . . 14
|
214 | 212, 212,
213 | cnmptc 21465 |
. . . . . . . . . . . . 13
ℂfld ℂfld |
215 | | id 22 |
. . . . . . . . . . . . . . 15
|
216 | 212, 212,
215 | cnmptc 21465 |
. . . . . . . . . . . . . 14
ℂfld ℂfld |
217 | 212 | cnmptid 21464 |
. . . . . . . . . . . . . 14
ℂfld ℂfld |
218 | 210 | mulcn 22670 |
. . . . . . . . . . . . . . 15
ℂfld ℂfld ℂfld |
219 | 218 | a1i 11 |
. . . . . . . . . . . . . 14
ℂfld ℂfld ℂfld |
220 | 212, 216,
217, 219 | cnmpt12f 21469 |
. . . . . . . . . . . . 13
ℂfld ℂfld |
221 | 210 | addcn 22668 |
. . . . . . . . . . . . . 14
ℂfld ℂfld ℂfld |
222 | 221 | a1i 11 |
. . . . . . . . . . . . 13
ℂfld ℂfld ℂfld |
223 | 212, 214,
220, 222 | cnmpt12f 21469 |
. . . . . . . . . . . 12
ℂfld ℂfld |
224 | 209, 212,
46, 223 | cnmpt1res 21479 |
. . . . . . . . . . 11
ℂfld
↾t ℂfld |
225 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
226 | 145, 225 | fmptd 6385 |
. . . . . . . . . . . . 13
|
227 | | frn 6053 |
. . . . . . . . . . . . 13
|
228 | 226, 227 | syl 17 |
. . . . . . . . . . . 12
|
229 | | difss 3737 |
. . . . . . . . . . . . . 14
|
230 | 97, 229 | sstri 3612 |
. . . . . . . . . . . . 13
|
231 | 230 | a1i 11 |
. . . . . . . . . . . 12
|
232 | | cnrest2 21090 |
. . . . . . . . . . . 12
ℂfld
TopOn
ℂfld ↾t ℂfld
ℂfld ↾t ℂfld
↾t |
233 | 212, 228,
231, 232 | syl3anc 1326 |
. . . . . . . . . . 11
ℂfld
↾t ℂfld
ℂfld ↾t ℂfld
↾t |
234 | 224, 233 | mpbid 222 |
. . . . . . . . . 10
ℂfld
↾t ℂfld
↾t |
235 | | blcntr 22218 |
. . . . . . . . . . . . 13
|
236 | 32, 33, 42, 235 | syl3anc 1326 |
. . . . . . . . . . . 12
|
237 | 236, 30 | syl6eleqr 2712 |
. . . . . . . . . . 11
|
238 | | resttopon 20965 |
. . . . . . . . . . . . 13
ℂfld
TopOn ℂfld
↾t TopOn |
239 | 211, 46, 238 | sylancr 695 |
. . . . . . . . . . . 12
ℂfld
↾t TopOn |
240 | | toponuni 20719 |
. . . . . . . . . . . 12
ℂfld
↾t TopOn ℂfld ↾t |
241 | 239, 240 | syl 17 |
. . . . . . . . . . 11
ℂfld ↾t |
242 | 237, 241 | eleqtrd 2703 |
. . . . . . . . . 10
ℂfld ↾t |
243 | | eqid 2622 |
. . . . . . . . . . 11
ℂfld
↾t ℂfld
↾t |
244 | 243 | cncnpi 21082 |
. . . . . . . . . 10
ℂfld
↾t ℂfld
↾t
ℂfld
↾t ℂfld ↾t
ℂfld ↾t |
245 | 234, 242,
244 | syl2anc 693 |
. . . . . . . . 9
ℂfld
↾t ℂfld
↾t |
246 | | cnelprrecn 10029 |
. . . . . . . . . . 11
|
247 | | logf1o 24311 |
. . . . . . . . . . . . . 14
|
248 | | f1of 6137 |
. . . . . . . . . . . . . 14
|
249 | 247, 248 | ax-mp 5 |
. . . . . . . . . . . . 13
|
250 | | logrncn 24309 |
. . . . . . . . . . . . . 14
|
251 | 250 | ssriv 3607 |
. . . . . . . . . . . . 13
|
252 | | fss 6056 |
. . . . . . . . . . . . 13
|
253 | 249, 251,
252 | mp2an 708 |
. . . . . . . . . . . 12
|
254 | | fssres 6070 |
. . . . . . . . . . . 12
|
255 | 253, 97, 254 | mp2an 708 |
. . . . . . . . . . 11
|
256 | | blcntr 22218 |
. . . . . . . . . . . . . 14
|
257 | 31, 88, 139, 256 | mp3an 1424 |
. . . . . . . . . . . . 13
|
258 | | ovex 6678 |
. . . . . . . . . . . . . 14
|
259 | 93 | dvlog2 24399 |
. . . . . . . . . . . . . 14
|
260 | 258, 259 | dmmpti 6023 |
. . . . . . . . . . . . 13
|
261 | 257, 260 | eleqtrri 2700 |
. . . . . . . . . . . 12
|
262 | | eqid 2622 |
. . . . . . . . . . . . 13
ℂfld ↾t ℂfld ↾t |
263 | 259 | fveq1i 6192 |
. . . . . . . . . . . . . . . . 17
|
264 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
|
265 | | 1div1e1 10717 |
. . . . . . . . . . . . . . . . . . . 20
|
266 | 264, 265 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
|
267 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
|
268 | | 1ex 10035 |
. . . . . . . . . . . . . . . . . . 19
|
269 | 266, 267,
268 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . 18
|
270 | 257, 269 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
271 | 263, 270 | eqtr2i 2645 |
. . . . . . . . . . . . . . . 16
|
272 | 271 | a1i 11 |
. . . . . . . . . . . . . . 15
|
273 | | fvres 6207 |
. . . . . . . . . . . . . . . . . 18
|
274 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . 20
|
275 | 257, 274 | mp1i 13 |
. . . . . . . . . . . . . . . . . . 19
|
276 | | log1 24332 |
. . . . . . . . . . . . . . . . . . 19
|
277 | 275, 276 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . 18
|
278 | 273, 277 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
|
279 | 97 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . 20
|
280 | | eldifsn 4317 |
. . . . . . . . . . . . . . . . . . . 20
|
281 | 279, 280 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
|
282 | | logcl 24315 |
. . . . . . . . . . . . . . . . . . 19
|
283 | 281, 282 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
284 | 283 | subid1d 10381 |
. . . . . . . . . . . . . . . . 17
|
285 | 278, 284 | eqtr2d 2657 |
. . . . . . . . . . . . . . . 16
|
286 | 285 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
287 | 272, 286 | ifeq12d 4106 |
. . . . . . . . . . . . . 14
|
288 | 287 | mpteq2ia 4740 |
. . . . . . . . . . . . 13
|
289 | 262, 210,
288 | dvcnp 23682 |
. . . . . . . . . . . 12
ℂfld ↾t ℂfld |
290 | 261, 289 | mpan2 707 |
. . . . . . . . . . 11
ℂfld
↾t ℂfld |
291 | 246, 255,
230, 290 | mp3an 1424 |
. . . . . . . . . 10
ℂfld ↾t ℂfld |
292 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
|
293 | 292 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
294 | | ovex 6678 |
. . . . . . . . . . . . . 14
|
295 | 293, 225,
294 | fvmpt 6282 |
. . . . . . . . . . . . 13
|
296 | 237, 295 | syl 17 |
. . . . . . . . . . . 12
|
297 | | mul01 10215 |
. . . . . . . . . . . . . 14
|
298 | 297 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
299 | 298, 63 | syl6eq 2672 |
. . . . . . . . . . . 12
|
300 | 296, 299 | eqtrd 2656 |
. . . . . . . . . . 11
|
301 | 300 | fveq2d 6195 |
. . . . . . . . . 10
ℂfld ↾t ℂfld ℂfld ↾t ℂfld |
302 | 291, 301 | syl5eleqr 2708 |
. . . . . . . . 9
ℂfld
↾t ℂfld |
303 | | cnpco 21071 |
. . . . . . . . 9
ℂfld ↾t
ℂfld ↾t
ℂfld ↾t ℂfld ℂfld ↾t
ℂfld |
304 | 245, 302,
303 | syl2anc 693 |
. . . . . . . 8
ℂfld
↾t ℂfld |
305 | 208, 304 | eqeltrrd 2702 |
. . . . . . 7
ℂfld ↾t
ℂfld |
306 | 212, 212,
215 | cnmptc 21465 |
. . . . . . . . . 10
ℂfld ℂfld |
307 | 212 | cnmptid 21464 |
. . . . . . . . . 10
ℂfld ℂfld |
308 | 212, 306,
307, 219 | cnmpt12f 21469 |
. . . . . . . . 9
ℂfld ℂfld |
309 | | efcn 24197 |
. . . . . . . . . . 11
|
310 | 210 | cncfcn1 22713 |
. . . . . . . . . . 11
ℂfld
ℂfld |
311 | 309, 310 | eleqtri 2699 |
. . . . . . . . . 10
ℂfld
ℂfld |
312 | 311 | a1i 11 |
. . . . . . . . 9
ℂfld
ℂfld |
313 | 212, 308,
312 | cnmpt11f 21467 |
. . . . . . . 8
ℂfld ℂfld |
314 | | eqid 2622 |
. . . . . . . . . 10
|
315 | 181, 314 | fmptd 6385 |
. . . . . . . . 9
|
316 | 315, 237 | ffvelrnd 6360 |
. . . . . . . 8
|
317 | 211 | toponunii 20721 |
. . . . . . . . 9
ℂfld |
318 | 317 | cncnpi 21082 |
. . . . . . . 8
ℂfld ℂfld
ℂfld
ℂfld |
319 | 313, 316,
318 | syl2anc 693 |
. . . . . . 7
ℂfld
ℂfld |
320 | | cnpco 21071 |
. . . . . . 7
ℂfld ↾t
ℂfld ℂfld
ℂfld
ℂfld ↾t ℂfld |
321 | 305, 319,
320 | syl2anc 693 |
. . . . . 6
ℂfld ↾t
ℂfld |
322 | 193, 321 | eqeltrd 2701 |
. . . . 5
ℂfld
↾t ℂfld |
323 | 210 | cnfldtop 22587 |
. . . . . . 7
ℂfld |
324 | 323 | a1i 11 |
. . . . . 6
ℂfld |
325 | 210 | cnfldtopn 22585 |
. . . . . . . . . . 11
ℂfld |
326 | 325 | blopn 22305 |
. . . . . . . . . 10
ℂfld |
327 | 32, 33, 43, 326 | syl3anc 1326 |
. . . . . . . . 9
ℂfld |
328 | 30, 327 | syl5eqel 2705 |
. . . . . . . 8
ℂfld |
329 | | isopn3i 20886 |
. . . . . . . 8
ℂfld
ℂfld
ℂfld |
330 | 323, 328,
329 | sylancr 695 |
. . . . . . 7
ℂfld |
331 | 237, 330 | eleqtrrd 2704 |
. . . . . 6
ℂfld |
332 | | efcl 14813 |
. . . . . . . . 9
|
333 | 332 | ad2antrr 762 |
. . . . . . . 8
|
334 | 88, 14, 90 | sylancr 695 |
. . . . . . . . 9
|
335 | 334, 53 | cxpcld 24454 |
. . . . . . . 8
|
336 | 333, 335 | ifclda 4120 |
. . . . . . 7
|
337 | | eqid 2622 |
. . . . . . 7
|
338 | 336, 337 | fmptd 6385 |
. . . . . 6
|
339 | 317, 317 | cnprest 21093 |
. . . . . 6
ℂfld
ℂfld
ℂfld
ℂfld ℂfld
↾t ℂfld |
340 | 324, 46, 331, 338, 339 | syl22anc 1327 |
. . . . 5
ℂfld
ℂfld ℂfld
↾t ℂfld |
341 | 322, 340 | mpbird 247 |
. . . 4
ℂfld
ℂfld |
342 | 317 | cnpresti 21092 |
. . . 4
ℂfld
ℂfld
ℂfld
↾t ℂfld |
343 | 25, 27, 341, 342 | syl3anc 1326 |
. . 3
ℂfld
↾t ℂfld |
344 | 24, 343 | eqeltrd 2701 |
. 2
ℂfld ↾t
ℂfld |
345 | | simpl 473 |
. . . . . 6
|
346 | | rpcn 11841 |
. . . . . . 7
|
347 | 346 | adantl 482 |
. . . . . 6
|
348 | | rpne0 11848 |
. . . . . . 7
|
349 | 348 | adantl 482 |
. . . . . 6
|
350 | 345, 347,
349 | divcld 10801 |
. . . . 5
|
351 | | addcl 10018 |
. . . . 5
|
352 | 88, 350, 351 | sylancr 695 |
. . . 4
|
353 | 352, 347 | cxpcld 24454 |
. . 3
|
354 | | oveq2 6658 |
. . . . 5
|
355 | 354 | oveq2d 6666 |
. . . 4
|
356 | | id 22 |
. . . 4
|
357 | 355, 356 | oveq12d 6668 |
. . 3
|
358 | | eqid 2622 |
. . 3
ℂfld ↾t ℂfld
↾t |
359 | 332, 353,
357, 210, 358 | rlimcnp3 24694 |
. 2
ℂfld ↾t ℂfld |
360 | 344, 359 | mpbird 247 |
1
|