Step | Hyp | Ref
| Expression |
1 | | dvadd.bf |
. . . . . 6
|
2 | | eqid 2622 |
. . . . . . 7
↾t ↾t |
3 | | dvadd.j |
. . . . . . 7
ℂfld |
4 | | eqid 2622 |
. . . . . . 7
|
5 | | dvaddbr.s |
. . . . . . 7
|
6 | | dvadd.f |
. . . . . . 7
|
7 | | dvadd.x |
. . . . . . 7
|
8 | 2, 3, 4, 5, 6, 7 | eldv 23662 |
. . . . . 6
↾t lim |
9 | 1, 8 | mpbid 222 |
. . . . 5
↾t lim |
10 | 9 | simpld 475 |
. . . 4
↾t |
11 | | dvadd.bg |
. . . . . 6
|
12 | | eqid 2622 |
. . . . . . 7
|
13 | | dvadd.g |
. . . . . . 7
|
14 | | dvadd.y |
. . . . . . 7
|
15 | 2, 3, 12, 5, 13, 14 | eldv 23662 |
. . . . . 6
↾t lim |
16 | 11, 15 | mpbid 222 |
. . . . 5
↾t lim |
17 | 16 | simpld 475 |
. . . 4
↾t |
18 | 10, 17 | elind 3798 |
. . 3
↾t ↾t |
19 | 3 | cnfldtopon 22586 |
. . . . . 6
TopOn |
20 | | resttopon 20965 |
. . . . . 6
TopOn
↾t TopOn |
21 | 19, 5, 20 | sylancr 695 |
. . . . 5
↾t TopOn |
22 | | topontop 20718 |
. . . . 5
↾t TopOn ↾t |
23 | 21, 22 | syl 17 |
. . . 4
↾t |
24 | | toponuni 20719 |
. . . . . 6
↾t TopOn ↾t |
25 | 21, 24 | syl 17 |
. . . . 5
↾t |
26 | 7, 25 | sseqtrd 3641 |
. . . 4
↾t |
27 | 14, 25 | sseqtrd 3641 |
. . . 4
↾t |
28 | | eqid 2622 |
. . . . 5
↾t
↾t |
29 | 28 | ntrin 20865 |
. . . 4
↾t
↾t ↾t
↾t ↾t
↾t |
30 | 23, 26, 27, 29 | syl3anc 1326 |
. . 3
↾t
↾t ↾t |
31 | 18, 30 | eleqtrrd 2704 |
. 2
↾t |
32 | 6 | adantr 481 |
. . . . . . . 8
|
33 | | inss1 3833 |
. . . . . . . . 9
|
34 | | eldifi 3732 |
. . . . . . . . . 10
|
35 | 34 | adantl 482 |
. . . . . . . . 9
|
36 | 33, 35 | sseldi 3601 |
. . . . . . . 8
|
37 | 32, 36 | ffvelrnd 6360 |
. . . . . . 7
|
38 | 5, 6, 7 | dvbss 23665 |
. . . . . . . . . 10
|
39 | | reldv 23634 |
. . . . . . . . . . 11
|
40 | | releldm 5358 |
. . . . . . . . . . 11
|
41 | 39, 1, 40 | sylancr 695 |
. . . . . . . . . 10
|
42 | 38, 41 | sseldd 3604 |
. . . . . . . . 9
|
43 | 6, 42 | ffvelrnd 6360 |
. . . . . . . 8
|
44 | 43 | adantr 481 |
. . . . . . 7
|
45 | 37, 44 | subcld 10392 |
. . . . . 6
|
46 | 7, 5 | sstrd 3613 |
. . . . . . . . 9
|
47 | 46 | adantr 481 |
. . . . . . . 8
|
48 | 47, 36 | sseldd 3604 |
. . . . . . 7
|
49 | 46, 42 | sseldd 3604 |
. . . . . . . 8
|
50 | 49 | adantr 481 |
. . . . . . 7
|
51 | 48, 50 | subcld 10392 |
. . . . . 6
|
52 | | eldifsni 4320 |
. . . . . . . 8
|
53 | 52 | adantl 482 |
. . . . . . 7
|
54 | 48, 50, 53 | subne0d 10401 |
. . . . . 6
|
55 | 45, 51, 54 | divcld 10801 |
. . . . 5
|
56 | 13 | adantr 481 |
. . . . . 6
|
57 | | inss2 3834 |
. . . . . . 7
|
58 | 57, 35 | sseldi 3601 |
. . . . . 6
|
59 | 56, 58 | ffvelrnd 6360 |
. . . . 5
|
60 | 55, 59 | mulcld 10060 |
. . . 4
|
61 | | ssdif 3745 |
. . . . . . . 8
|
62 | 57, 61 | mp1i 13 |
. . . . . . 7
|
63 | 62 | sselda 3603 |
. . . . . 6
|
64 | 14, 5 | sstrd 3613 |
. . . . . . 7
|
65 | 5, 13, 14 | dvbss 23665 |
. . . . . . . 8
|
66 | | reldv 23634 |
. . . . . . . . 9
|
67 | | releldm 5358 |
. . . . . . . . 9
|
68 | 66, 11, 67 | sylancr 695 |
. . . . . . . 8
|
69 | 65, 68 | sseldd 3604 |
. . . . . . 7
|
70 | 13, 64, 69 | dvlem 23660 |
. . . . . 6
|
71 | 63, 70 | syldan 487 |
. . . . 5
|
72 | 71, 44 | mulcld 10060 |
. . . 4
|
73 | | ssid 3624 |
. . . . 5
|
74 | 73 | a1i 11 |
. . . 4
|
75 | | txtopon 21394 |
. . . . . . 7
TopOn
TopOn
TopOn |
76 | 19, 19, 75 | mp2an 708 |
. . . . . 6
TopOn |
77 | 76 | toponunii 20721 |
. . . . . . 7
|
78 | 77 | restid 16094 |
. . . . . 6
TopOn ↾t |
79 | 76, 78 | ax-mp 5 |
. . . . 5
↾t |
80 | 79 | eqcomi 2631 |
. . . 4
↾t |
81 | 9 | simprd 479 |
. . . . . 6
lim |
82 | 6, 46, 42 | dvlem 23660 |
. . . . . . . . 9
|
83 | 82, 4 | fmptd 6385 |
. . . . . . . 8
|
84 | | ssdif 3745 |
. . . . . . . . 9
|
85 | 33, 84 | mp1i 13 |
. . . . . . . 8
|
86 | 46 | ssdifssd 3748 |
. . . . . . . 8
|
87 | | eqid 2622 |
. . . . . . . 8
↾t
↾t |
88 | 33, 7 | syl5ss 3614 |
. . . . . . . . . . . . . . 15
|
89 | 88, 25 | sseqtrd 3641 |
. . . . . . . . . . . . . 14
↾t |
90 | | difssd 3738 |
. . . . . . . . . . . . . 14
↾t ↾t |
91 | 89, 90 | unssd 3789 |
. . . . . . . . . . . . 13
↾t ↾t |
92 | | ssun1 3776 |
. . . . . . . . . . . . . 14
↾t |
93 | 92 | a1i 11 |
. . . . . . . . . . . . 13
↾t |
94 | 28 | ntrss 20859 |
. . . . . . . . . . . . 13
↾t
↾t ↾t
↾t ↾t
↾t ↾t |
95 | 23, 91, 93, 94 | syl3anc 1326 |
. . . . . . . . . . . 12
↾t
↾t ↾t |
96 | 95, 31 | sseldd 3604 |
. . . . . . . . . . 11
↾t
↾t |
97 | 96, 42 | elind 3798 |
. . . . . . . . . 10
↾t
↾t |
98 | 33 | a1i 11 |
. . . . . . . . . . . 12
|
99 | | eqid 2622 |
. . . . . . . . . . . . 13
↾t
↾t
↾t
↾t |
100 | 28, 99 | restntr 20986 |
. . . . . . . . . . . 12
↾t
↾t
↾t
↾t
↾t
↾t |
101 | 23, 26, 98, 100 | syl3anc 1326 |
. . . . . . . . . . 11
↾t
↾t
↾t
↾t |
102 | 3 | cnfldtop 22587 |
. . . . . . . . . . . . . . 15
|
103 | 102 | a1i 11 |
. . . . . . . . . . . . . 14
|
104 | | cnex 10017 |
. . . . . . . . . . . . . . 15
|
105 | | ssexg 4804 |
. . . . . . . . . . . . . . 15
|
106 | 5, 104, 105 | sylancl 694 |
. . . . . . . . . . . . . 14
|
107 | | restabs 20969 |
. . . . . . . . . . . . . 14
↾t
↾t ↾t |
108 | 103, 7, 106, 107 | syl3anc 1326 |
. . . . . . . . . . . . 13
↾t ↾t ↾t |
109 | 108 | fveq2d 6195 |
. . . . . . . . . . . 12
↾t
↾t ↾t |
110 | 109 | fveq1d 6193 |
. . . . . . . . . . 11
↾t
↾t
↾t |
111 | 101, 110 | eqtr3d 2658 |
. . . . . . . . . 10
↾t
↾t ↾t
|
112 | 97, 111 | eleqtrd 2703 |
. . . . . . . . 9
↾t |
113 | | undif1 4043 |
. . . . . . . . . . . . 13
|
114 | 42 | snssd 4340 |
. . . . . . . . . . . . . 14
|
115 | | ssequn2 3786 |
. . . . . . . . . . . . . 14
|
116 | 114, 115 | sylib 208 |
. . . . . . . . . . . . 13
|
117 | 113, 116 | syl5eq 2668 |
. . . . . . . . . . . 12
|
118 | 117 | oveq2d 6666 |
. . . . . . . . . . 11
↾t
↾t |
119 | 118 | fveq2d 6195 |
. . . . . . . . . 10
↾t ↾t |
120 | | undif1 4043 |
. . . . . . . . . . 11
|
121 | 42, 69 | elind 3798 |
. . . . . . . . . . . . 13
|
122 | 121 | snssd 4340 |
. . . . . . . . . . . 12
|
123 | | ssequn2 3786 |
. . . . . . . . . . . 12
|
124 | 122, 123 | sylib 208 |
. . . . . . . . . . 11
|
125 | 120, 124 | syl5eq 2668 |
. . . . . . . . . 10
|
126 | 119, 125 | fveq12d 6197 |
. . . . . . . . 9
↾t ↾t
|
127 | 112, 126 | eleqtrrd 2704 |
. . . . . . . 8
↾t |
128 | 83, 85, 86, 3, 87, 127 | limcres 23650 |
. . . . . . 7
lim lim |
129 | 85 | resmptd 5452 |
. . . . . . . 8
|
130 | 129 | oveq1d 6665 |
. . . . . . 7
lim lim |
131 | 128, 130 | eqtr3d 2658 |
. . . . . 6
lim lim |
132 | 81, 131 | eleqtrd 2703 |
. . . . 5
lim |
133 | | eqid 2622 |
. . . . . . . . . 10
↾t ↾t |
134 | 133, 3 | dvcnp2 23683 |
. . . . . . . . 9
↾t |
135 | 5, 13, 14, 68, 134 | syl31anc 1329 |
. . . . . . . 8
↾t |
136 | 3, 133 | cnplimc 23651 |
. . . . . . . . 9
↾t lim |
137 | 64, 69, 136 | syl2anc 693 |
. . . . . . . 8
↾t
lim |
138 | 135, 137 | mpbid 222 |
. . . . . . 7
lim |
139 | 138 | simprd 479 |
. . . . . 6
lim |
140 | | difss 3737 |
. . . . . . . . . 10
|
141 | 140, 57 | sstri 3612 |
. . . . . . . . 9
|
142 | 141 | a1i 11 |
. . . . . . . 8
|
143 | | eqid 2622 |
. . . . . . . 8
↾t
↾t |
144 | | difssd 3738 |
. . . . . . . . . . . . . 14
↾t ↾t |
145 | 89, 144 | unssd 3789 |
. . . . . . . . . . . . 13
↾t ↾t |
146 | | ssun1 3776 |
. . . . . . . . . . . . . 14
↾t |
147 | 146 | a1i 11 |
. . . . . . . . . . . . 13
↾t |
148 | 28 | ntrss 20859 |
. . . . . . . . . . . . 13
↾t
↾t ↾t
↾t ↾t
↾t ↾t |
149 | 23, 145, 147, 148 | syl3anc 1326 |
. . . . . . . . . . . 12
↾t
↾t ↾t |
150 | 149, 31 | sseldd 3604 |
. . . . . . . . . . 11
↾t
↾t |
151 | 150, 69 | elind 3798 |
. . . . . . . . . 10
↾t
↾t |
152 | 57 | a1i 11 |
. . . . . . . . . . . 12
|
153 | | eqid 2622 |
. . . . . . . . . . . . 13
↾t
↾t
↾t
↾t |
154 | 28, 153 | restntr 20986 |
. . . . . . . . . . . 12
↾t
↾t
↾t
↾t
↾t
↾t |
155 | 23, 27, 152, 154 | syl3anc 1326 |
. . . . . . . . . . 11
↾t
↾t
↾t
↾t |
156 | | restabs 20969 |
. . . . . . . . . . . . . 14
↾t
↾t ↾t |
157 | 103, 14, 106, 156 | syl3anc 1326 |
. . . . . . . . . . . . 13
↾t ↾t ↾t |
158 | 157 | fveq2d 6195 |
. . . . . . . . . . . 12
↾t
↾t ↾t |
159 | 158 | fveq1d 6193 |
. . . . . . . . . . 11
↾t
↾t
↾t |
160 | 155, 159 | eqtr3d 2658 |
. . . . . . . . . 10
↾t
↾t ↾t
|
161 | 151, 160 | eleqtrd 2703 |
. . . . . . . . 9
↾t |
162 | 69 | snssd 4340 |
. . . . . . . . . . . . 13
|
163 | | ssequn2 3786 |
. . . . . . . . . . . . 13
|
164 | 162, 163 | sylib 208 |
. . . . . . . . . . . 12
|
165 | 164 | oveq2d 6666 |
. . . . . . . . . . 11
↾t ↾t |
166 | 165 | fveq2d 6195 |
. . . . . . . . . 10
↾t
↾t |
167 | 166, 125 | fveq12d 6197 |
. . . . . . . . 9
↾t
↾t
|
168 | 161, 167 | eleqtrrd 2704 |
. . . . . . . 8
↾t |
169 | 13, 142, 64, 3, 143, 168 | limcres 23650 |
. . . . . . 7
lim lim |
170 | 13, 142 | feqresmpt 6250 |
. . . . . . . 8
|
171 | 170 | oveq1d 6665 |
. . . . . . 7
lim
lim |
172 | 169, 171 | eqtr3d 2658 |
. . . . . 6
lim lim |
173 | 139, 172 | eleqtrd 2703 |
. . . . 5
lim |
174 | 3 | mulcn 22670 |
. . . . . 6
|
175 | 5, 6, 7 | dvcl 23663 |
. . . . . . . 8
|
176 | 1, 175 | mpdan 702 |
. . . . . . 7
|
177 | 13, 69 | ffvelrnd 6360 |
. . . . . . 7
|
178 | | opelxpi 5148 |
. . . . . . 7
|
179 | 176, 177,
178 | syl2anc 693 |
. . . . . 6
|
180 | 77 | cncnpi 21082 |
. . . . . 6
|
181 | 174, 179,
180 | sylancr 695 |
. . . . 5
|
182 | 55, 59, 74, 74, 3, 80, 132, 173, 181 | limccnp2 23656 |
. . . 4
lim |
183 | 16 | simprd 479 |
. . . . . 6
lim |
184 | 70, 12 | fmptd 6385 |
. . . . . . . 8
|
185 | 64 | ssdifssd 3748 |
. . . . . . . 8
|
186 | | eqid 2622 |
. . . . . . . 8
↾t
↾t |
187 | | undif1 4043 |
. . . . . . . . . . . . 13
|
188 | 187, 164 | syl5eq 2668 |
. . . . . . . . . . . 12
|
189 | 188 | oveq2d 6666 |
. . . . . . . . . . 11
↾t
↾t |
190 | 189 | fveq2d 6195 |
. . . . . . . . . 10
↾t ↾t |
191 | 190, 125 | fveq12d 6197 |
. . . . . . . . 9
↾t ↾t
|
192 | 161, 191 | eleqtrrd 2704 |
. . . . . . . 8
↾t |
193 | 184, 62, 185, 3, 186, 192 | limcres 23650 |
. . . . . . 7
lim lim |
194 | 62 | resmptd 5452 |
. . . . . . . 8
|
195 | 194 | oveq1d 6665 |
. . . . . . 7
lim lim |
196 | 193, 195 | eqtr3d 2658 |
. . . . . 6
lim lim |
197 | 183, 196 | eleqtrd 2703 |
. . . . 5
lim |
198 | 88, 5 | sstrd 3613 |
. . . . . . . 8
|
199 | | cncfmptc 22714 |
. . . . . . . 8
|
200 | 43, 198, 74, 199 | syl3anc 1326 |
. . . . . . 7
|
201 | | eqidd 2623 |
. . . . . . 7
|
202 | 200, 121,
201 | cnmptlimc 23654 |
. . . . . 6
lim |
203 | 43 | adantr 481 |
. . . . . . . . 9
|
204 | | eqid 2622 |
. . . . . . . . 9
|
205 | 203, 204 | fmptd 6385 |
. . . . . . . 8
|
206 | 205 | limcdif 23640 |
. . . . . . 7
lim lim |
207 | | resmpt 5449 |
. . . . . . . . 9
|
208 | 140, 207 | mp1i 13 |
. . . . . . . 8
|
209 | 208 | oveq1d 6665 |
. . . . . . 7
lim
lim |
210 | 206, 209 | eqtrd 2656 |
. . . . . 6
lim
lim |
211 | 202, 210 | eleqtrd 2703 |
. . . . 5
lim |
212 | 5, 13, 14 | dvcl 23663 |
. . . . . . . 8
|
213 | 11, 212 | mpdan 702 |
. . . . . . 7
|
214 | | opelxpi 5148 |
. . . . . . 7
|
215 | 213, 43, 214 | syl2anc 693 |
. . . . . 6
|
216 | 77 | cncnpi 21082 |
. . . . . 6
|
217 | 174, 215,
216 | sylancr 695 |
. . . . 5
|
218 | 71, 44, 74, 74, 3, 80, 197, 211, 217 | limccnp2 23656 |
. . . 4
lim |
219 | 3 | addcn 22668 |
. . . . 5
|
220 | 176, 177 | mulcld 10060 |
. . . . . 6
|
221 | 213, 43 | mulcld 10060 |
. . . . . 6
|
222 | | opelxpi 5148 |
. . . . . 6
|
223 | 220, 221,
222 | syl2anc 693 |
. . . . 5
|
224 | 77 | cncnpi 21082 |
. . . . 5
|
225 | 219, 223,
224 | sylancr 695 |
. . . 4
|
226 | 60, 72, 74, 74, 3, 80, 182, 218, 225 | limccnp2 23656 |
. . 3
lim |
227 | 42 | adantr 481 |
. . . . . . . . . 10
|
228 | 32, 227 | ffvelrnd 6360 |
. . . . . . . . 9
|
229 | 37, 228 | subcld 10392 |
. . . . . . . 8
|
230 | 229, 59 | mulcld 10060 |
. . . . . . 7
|
231 | 69 | adantr 481 |
. . . . . . . . . 10
|
232 | 56, 231 | ffvelrnd 6360 |
. . . . . . . . 9
|
233 | 59, 232 | subcld 10392 |
. . . . . . . 8
|
234 | 233, 228 | mulcld 10060 |
. . . . . . 7
|
235 | 47, 227 | sseldd 3604 |
. . . . . . . 8
|
236 | 48, 235 | subcld 10392 |
. . . . . . 7
|
237 | 230, 234,
236, 54 | divdird 10839 |
. . . . . 6
|
238 | 37, 59 | mulcld 10060 |
. . . . . . . . 9
|
239 | 228, 59 | mulcld 10060 |
. . . . . . . . 9
|
240 | 228, 232 | mulcld 10060 |
. . . . . . . . 9
|
241 | 238, 239,
240 | npncand 10416 |
. . . . . . . 8
|
242 | 37, 228, 59 | subdird 10487 |
. . . . . . . . 9
|
243 | 233, 228 | mulcomd 10061 |
. . . . . . . . . 10
|
244 | 228, 59, 232 | subdid 10486 |
. . . . . . . . . 10
|
245 | 243, 244 | eqtrd 2656 |
. . . . . . . . 9
|
246 | 242, 245 | oveq12d 6668 |
. . . . . . . 8
|
247 | | ffn 6045 |
. . . . . . . . . . . . 13
|
248 | 6, 247 | syl 17 |
. . . . . . . . . . . 12
|
249 | 248 | adantr 481 |
. . . . . . . . . . 11
|
250 | | ffn 6045 |
. . . . . . . . . . . . 13
|
251 | 13, 250 | syl 17 |
. . . . . . . . . . . 12
|
252 | 251 | adantr 481 |
. . . . . . . . . . 11
|
253 | | ssexg 4804 |
. . . . . . . . . . . . 13
|
254 | 46, 104, 253 | sylancl 694 |
. . . . . . . . . . . 12
|
255 | 254 | adantr 481 |
. . . . . . . . . . 11
|
256 | | ssexg 4804 |
. . . . . . . . . . . . 13
|
257 | 64, 104, 256 | sylancl 694 |
. . . . . . . . . . . 12
|
258 | 257 | adantr 481 |
. . . . . . . . . . 11
|
259 | | eqid 2622 |
. . . . . . . . . . 11
|
260 | | eqidd 2623 |
. . . . . . . . . . 11
|
261 | | eqidd 2623 |
. . . . . . . . . . 11
|
262 | 249, 252,
255, 258, 259, 260, 261 | ofval 6906 |
. . . . . . . . . 10
|
263 | 35, 262 | mpdan 702 |
. . . . . . . . 9
|
264 | | eqidd 2623 |
. . . . . . . . . . 11
|
265 | | eqidd 2623 |
. . . . . . . . . . 11
|
266 | 249, 252,
255, 258, 259, 264, 265 | ofval 6906 |
. . . . . . . . . 10
|
267 | 121, 266 | mpidan 704 |
. . . . . . . . 9
|
268 | 263, 267 | oveq12d 6668 |
. . . . . . . 8
|
269 | 241, 246,
268 | 3eqtr4d 2666 |
. . . . . . 7
|
270 | 269 | oveq1d 6665 |
. . . . . 6
|
271 | 229, 59, 236, 54 | div23d 10838 |
. . . . . . 7
|
272 | 233, 228,
236, 54 | div23d 10838 |
. . . . . . 7
|
273 | 271, 272 | oveq12d 6668 |
. . . . . 6
|
274 | 237, 270,
273 | 3eqtr3d 2664 |
. . . . 5
|
275 | 274 | mpteq2dva 4744 |
. . . 4
|
276 | 275 | oveq1d 6665 |
. . 3
lim
lim |
277 | 226, 276 | eleqtrrd 2704 |
. 2
lim |
278 | | eqid 2622 |
. . 3
|
279 | | mulcl 10020 |
. . . . 5
|
280 | 279 | adantl 482 |
. . . 4
|
281 | 280, 6, 13, 254, 257, 259 | off 6912 |
. . 3
|
282 | 2, 3, 278, 5, 281, 88 | eldv 23662 |
. 2
↾t
lim |
283 | 31, 277, 282 | mpbir2and 957 |
1
|