Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  efrlim Structured version   Unicode version

Theorem efrlim 20810
 Description: The limit of the sequence is the exponential function. This is often taken as an alternate definition of the exponential function (see also dfef2 20811). (Contributed by Mario Carneiro, 1-Mar-2015.)
Hypothesis
Ref Expression
efrlim.1
Assertion
Ref Expression
efrlim
Distinct variable group:   ,
Allowed substitution hint:   ()

Proof of Theorem efrlim
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0re 9093 . . . . . . . . 9
2 pnfxr 10715 . . . . . . . . 9
3 icossre 10993 . . . . . . . . 9
41, 2, 3mp2an 655 . . . . . . . 8
5 ax-resscn 9049 . . . . . . . 8
64, 5sstri 3359 . . . . . . 7
76sseli 3346 . . . . . 6
8 simpll 732 . . . . . . . . . . 11
9 ax-1cn 9050 . . . . . . . . . . . 12
109a1i 11 . . . . . . . . . . 11
11 simplr 733 . . . . . . . . . . 11
12 ax-1ne0 9061 . . . . . . . . . . . 12
1312a1i 11 . . . . . . . . . . 11
14 simpr 449 . . . . . . . . . . . 12
1514neneqad 2676 . . . . . . . . . . 11
168, 10, 11, 13, 15divdiv2d 9824 . . . . . . . . . 10
17 mulcl 9076 . . . . . . . . . . . 12
1817adantr 453 . . . . . . . . . . 11
1918div1d 9784 . . . . . . . . . 10
2016, 19eqtrd 2470 . . . . . . . . 9
2120oveq2d 6099 . . . . . . . 8
2221oveq1d 6098 . . . . . . 7
2322ifeq2da 3767 . . . . . 6
247, 23sylan2 462 . . . . 5
2524mpteq2dva 4297 . . . 4
26 resmpt 5193 . . . . 5
276, 26ax-mp 8 . . . 4
2825, 27syl6eqr 2488 . . 3
296a1i 11 . . . 4
30 0le0 10083 . . . . . 6
31 elrege0 11009 . . . . . 6
321, 30, 31mpbir2an 888 . . . . 5
3332a1i 11 . . . 4
34 eqeq2 2447 . . . . . . . . 9
35 eqeq2 2447 . . . . . . . . 9
36 efrlim.1 . . . . . . . . . . . . . 14
37 cnxmet 18809 . . . . . . . . . . . . . . . 16
3837a1i 11 . . . . . . . . . . . . . . 15
39 0cn 9086 . . . . . . . . . . . . . . . 16
4039a1i 11 . . . . . . . . . . . . . . 15
41 abscl 12085 . . . . . . . . . . . . . . . . . . 19
42 peano2re 9241 . . . . . . . . . . . . . . . . . . 19
4341, 42syl 16 . . . . . . . . . . . . . . . . . 18
441a1i 11 . . . . . . . . . . . . . . . . . . 19
45 absge0 12094 . . . . . . . . . . . . . . . . . . 19
4641ltp1d 9943 . . . . . . . . . . . . . . . . . . 19
4744, 41, 43, 45, 46lelttrd 9230 . . . . . . . . . . . . . . . . . 18
4843, 47elrpd 10648 . . . . . . . . . . . . . . . . 17
4948rpreccld 10660 . . . . . . . . . . . . . . . 16
5049rpxrd 10651 . . . . . . . . . . . . . . 15
51 blssm 18450 . . . . . . . . . . . . . . 15
5238, 40, 50, 51syl3anc 1185 . . . . . . . . . . . . . 14
5336, 52syl5eqss 3394 . . . . . . . . . . . . 13
5453sselda 3350 . . . . . . . . . . . 12
55 mul0or 9664 . . . . . . . . . . . 12
5654, 55syldan 458 . . . . . . . . . . 11
5756biimpa 472 . . . . . . . . . 10
58 simpl 445 . . . . . . . . . . . . . . . . . . 19
5958, 54jca 520 . . . . . . . . . . . . . . . . . 18
6011, 15reccld 9785 . . . . . . . . . . . . . . . . . 18
6159, 60sylan 459 . . . . . . . . . . . . . . . . 17
6261adantlr 697 . . . . . . . . . . . . . . . 16
63621cxpd 20600 . . . . . . . . . . . . . . 15
64 simplr 733 . . . . . . . . . . . . . . . . . . . 20
6564oveq1d 6098 . . . . . . . . . . . . . . . . . . 19
6654ad2antrr 708 . . . . . . . . . . . . . . . . . . . 20
6766mul02d 9266 . . . . . . . . . . . . . . . . . . 19
6865, 67eqtrd 2470 . . . . . . . . . . . . . . . . . 18
6968oveq2d 6099 . . . . . . . . . . . . . . . . 17
709addid1i 9255 . . . . . . . . . . . . . . . . 17
7169, 70syl6eq 2486 . . . . . . . . . . . . . . . 16
7271oveq1d 6098 . . . . . . . . . . . . . . 15
7364fveq2d 5734 . . . . . . . . . . . . . . . 16
74 ef0 12695 . . . . . . . . . . . . . . . 16
7573, 74syl6eq 2486 . . . . . . . . . . . . . . 15
7663, 72, 753eqtr4d 2480 . . . . . . . . . . . . . 14
7776ifeq2da 3767 . . . . . . . . . . . . 13
78 ifid 3773 . . . . . . . . . . . . 13
7977, 78syl6eq 2486 . . . . . . . . . . . 12
80 iftrue 3747 . . . . . . . . . . . . 13
8180adantl 454 . . . . . . . . . . . 12
8279, 81jaodan 762 . . . . . . . . . . 11
83 mulid1 9090 . . . . . . . . . . . . 13
8483ad2antrr 708 . . . . . . . . . . . 12
8584fveq2d 5734 . . . . . . . . . . 11
8682, 85eqtr4d 2473 . . . . . . . . . 10
8757, 86syldan 458 . . . . . . . . 9
88 mulne0b 9665 . . . . . . . . . . . . 13
8954, 88syldan 458 . . . . . . . . . . . 12
90 df-ne 2603 . . . . . . . . . . . 12
9189, 90syl6bb 254 . . . . . . . . . . 11
92 simprr 735 . . . . . . . . . . . . . . 15
9392neneqd 2619 . . . . . . . . . . . . . 14
94 iffalse 3748 . . . . . . . . . . . . . 14
9593, 94syl 16 . . . . . . . . . . . . 13
9654, 17syldan 458 . . . . . . . . . . . . . . . 16
97 addcl 9074 . . . . . . . . . . . . . . . 16
989, 96, 97sylancr 646 . . . . . . . . . . . . . . 15
9998adantr 453 . . . . . . . . . . . . . 14
100 eqid 2438 . . . . . . . . . . . . . . . . . . 19
101100dvlog2lem 20545 . . . . . . . . . . . . . . . . . 18
102 eqid 2438 . . . . . . . . . . . . . . . . . . 19
103102logdmss 20535 . . . . . . . . . . . . . . . . . 18
104101, 103sstri 3359 . . . . . . . . . . . . . . . . 17
105 eqid 2438 . . . . . . . . . . . . . . . . . . . . . 22
106105cnmetdval 18807 . . . . . . . . . . . . . . . . . . . . 21
10798, 9, 106sylancl 645 . . . . . . . . . . . . . . . . . . . 20
108 pncan2 9314 . . . . . . . . . . . . . . . . . . . . . 22
1099, 96, 108sylancr 646 . . . . . . . . . . . . . . . . . . . . 21
110109fveq2d 5734 . . . . . . . . . . . . . . . . . . . 20
111107, 110eqtrd 2470 . . . . . . . . . . . . . . . . . . 19
11296abscld 12240 . . . . . . . . . . . . . . . . . . . 20
11343adantr 453 . . . . . . . . . . . . . . . . . . . . 21
11454abscld 12240 . . . . . . . . . . . . . . . . . . . . 21
115113, 114remulcld 9118 . . . . . . . . . . . . . . . . . . . 20
116 1re 9092 . . . . . . . . . . . . . . . . . . . . 21
117116a1i 11 . . . . . . . . . . . . . . . . . . . 20
118 absmul 12101 . . . . . . . . . . . . . . . . . . . . . 22
11954, 118syldan 458 . . . . . . . . . . . . . . . . . . . . 21
12041adantr 453 . . . . . . . . . . . . . . . . . . . . . 22
121120, 42syl 16 . . . . . . . . . . . . . . . . . . . . . 22
12254absge0d 12248 . . . . . . . . . . . . . . . . . . . . . 22
123120lep1d 9944 . . . . . . . . . . . . . . . . . . . . . 22
124120, 121, 114, 122, 123lemul1ad 9952 . . . . . . . . . . . . . . . . . . . . 21
125119, 124eqbrtrd 4234 . . . . . . . . . . . . . . . . . . . 20
126105cnmetdval 18807 . . . . . . . . . . . . . . . . . . . . . . . 24
12754, 39, 126sylancl 645 . . . . . . . . . . . . . . . . . . . . . . 23
12854subid1d 9402 . . . . . . . . . . . . . . . . . . . . . . . 24
129128fveq2d 5734 . . . . . . . . . . . . . . . . . . . . . . 23
130127, 129eqtrd 2470 . . . . . . . . . . . . . . . . . . . . . 22
131 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . 24
132131, 36syl6eleq 2528 . . . . . . . . . . . . . . . . . . . . . . 23
13337a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
13450adantr 453 . . . . . . . . . . . . . . . . . . . . . . . 24
13539a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
136 elbl3 18424 . . . . . . . . . . . . . . . . . . . . . . . 24
137133, 134, 135, 54, 136syl22anc 1186 . . . . . . . . . . . . . . . . . . . . . . 23
138132, 137mpbid 203 . . . . . . . . . . . . . . . . . . . . . 22
139130, 138eqbrtrrd 4236 . . . . . . . . . . . . . . . . . . . . 21
14047adantr 453 . . . . . . . . . . . . . . . . . . . . . 22
141 ltmuldiv2 9883 . . . . . . . . . . . . . . . . . . . . . 22
142114, 117, 121, 140, 141syl112anc 1189 . . . . . . . . . . . . . . . . . . . . 21
143139, 142mpbird 225 . . . . . . . . . . . . . . . . . . . 20
144112, 115, 117, 125, 143lelttrd 9230 . . . . . . . . . . . . . . . . . . 19
145111, 144eqbrtrd 4234 . . . . . . . . . . . . . . . . . 18
146 1rp 10618 . . . . . . . . . . . . . . . . . . . 20
147 rpxr 10621 . . . . . . . . . . . . . . . . . . . 20
148146, 147mp1i 12 . . . . . . . . . . . . . . . . . . 19
1499a1i 11 . . . . . . . . . . . . . . . . . . 19
150 elbl3 18424 . . . . . . . . . . . . . . . . . . 19
151133, 148, 149, 98, 150syl22anc 1186 . . . . . . . . . . . . . . . . . 18
152145, 151mpbird 225 . . . . . . . . . . . . . . . . 17
153104, 152sseldi 3348 . . . . . . . . . . . . . . . 16
154 eldifsni 3930 . . . . . . . . . . . . . . . 16
155153, 154syl 16 . . . . . . . . . . . . . . 15
156155adantr 453 . . . . . . . . . . . . . 14
15754adantr 453 . . . . . . . . . . . . . . 15
158157, 92reccld 9785 . . . . . . . . . . . . . 14
15999, 156, 158cxpefd 20605 . . . . . . . . . . . . 13
16098, 155logcld 20470 . . . . . . . . . . . . . . . . 17
161160adantr 453 . . . . . . . . . . . . . . . 16
162158, 161mulcomd 9111 . . . . . . . . . . . . . . 15
163 simpll 732 . . . . . . . . . . . . . . . . . . 19
164 simprl 734 . . . . . . . . . . . . . . . . . . 19
165163, 164dividd 9790 . . . . . . . . . . . . . . . . . 18
166165oveq1d 6098 . . . . . . . . . . . . . . . . 17
167163, 163, 157, 164, 92divdiv1d 9823 . . . . . . . . . . . . . . . . 17
168166, 167eqtr3d 2472 . . . . . . . . . . . . . . . 16
169168oveq2d 6099 . . . . . . . . . . . . . . 15
17096adantr 453 . . . . . . . . . . . . . . . 16
17189biimpa 472 . . . . . . . . . . . . . . . 16
172161, 163, 170, 171div12d 9828 . . . . . . . . . . . . . . 15
173162, 169, 1723eqtrd 2474 . . . . . . . . . . . . . 14
174173fveq2d 5734 . . . . . . . . . . . . 13
17595, 159, 1743eqtrd 2474 . . . . . . . . . . . 12
176175ex 425 . . . . . . . . . . 11
17791, 176sylbird 228 . . . . . . . . . 10
178177imp 420 . . . . . . . . 9
17934, 35, 87, 178ifbothda 3771 . . . . . . . 8
180179mpteq2dva 4297 . . . . . . 7
181 resmpt 5193 . . . . . . . 8
18253, 181syl 16 . . . . . . 7
1839a1i 11 . . . . . . . . 9
184160adantr 453 . . . . . . . . . 10
18596adantr 453 . . . . . . . . . 10
186 simpr 449 . . . . . . . . . . 11
187186neneqad 2676 . . . . . . . . . 10
188184, 185, 187divcld 9792 . . . . . . . . 9
189183, 188ifclda 3768 . . . . . . . 8
190 eqidd 2439 . . . . . . . 8
191 eqidd 2439 . . . . . . . 8
192 oveq2 6091 . . . . . . . . . 10
193192fveq2d 5734 . . . . . . . . 9
194 oveq2 6091 . . . . . . . . . . 11
195194fveq2d 5734 . . . . . . . . . 10
196 oveq2 6091 . . . . . . . . . . 11
197196fveq2d 5734 . . . . . . . . . 10
198195, 197ifsb 3750 . . . . . . . . 9
199193, 198syl6eq 2486 . . . . . . . 8
200189, 190, 191, 199fmptco 5903 . . . . . . 7
201180, 182, 2003eqtr4d 2480 . . . . . 6
202 eqidd 2439 . . . . . . . . . 10
203 eqidd 2439 . . . . . . . . . 10
204 eqeq1 2444 . . . . . . . . . . 11
205 fveq2 5730 . . . . . . . . . . . 12
206 oveq1 6090 . . . . . . . . . . . 12
207205, 206oveq12d 6101 . . . . . . . . . . 11
208204, 207ifbieq2d 3761 . . . . . . . . . 10
209152, 202, 203, 208fmptco 5903 . . . . . . . . 9
21070eqeq2i 2448 . . . . . . . . . . . 12
211149, 96, 135addcand 9271 . . . . . . . . . . . 12
212210, 211syl5bbr 252 . . . . . . . . . . 11
213109oveq2d 6099 . . . . . . . . . . 11
214212, 213ifbieq2d 3761 . . . . . . . . . 10
215214mpteq2dva 4297 . . . . . . . . 9
216209, 215eqtrd 2470 . . . . . . . 8
217 eqid 2438 . . . . . . . . . . . 12 fldt fldt
218 eqid 2438 . . . . . . . . . . . . . 14 fld fld
219218cnfldtopon 18819 . . . . . . . . . . . . 13 fld TopOn
220219a1i 11 . . . . . . . . . . . 12 fld TopOn
2219a1i 11 . . . . . . . . . . . . . 14
222220, 220, 221cnmptc 17696 . . . . . . . . . . . . 13 fld fld
223 id 21 . . . . . . . . . . . . . . 15
224220, 220, 223cnmptc 17696 . . . . . . . . . . . . . 14 fld fld
225220cnmptid 17695 . . . . . . . . . . . . . 14 fld fld
226218mulcn 18899 . . . . . . . . . . . . . . 15 fld fld fld
227226a1i 11 . . . . . . . . . . . . . 14 fld fld fld
228220, 224, 225, 227cnmpt12f 17700 . . . . . . . . . . . . 13 fld fld
229218addcn 18897 . . . . . . . . . . . . . 14 fld fld fld
230229a1i 11 . . . . . . . . . . . . 13 fld fld fld
231220, 222, 228, 230cnmpt12f 17700 . . . . . . . . . . . 12 fld fld
232217, 220, 53, 231cnmpt1res 17710 . . . . . . . . . . 11 fldt fld
233 eqid 2438 . . . . . . . . . . . . . 14
234152, 233fmptd 5895 . . . . . . . . . . . . 13
235 frn 5599 . . . . . . . . . . . . 13
236234, 235syl 16 . . . . . . . . . . . 12
237 difss 3476 . . . . . . . . . . . . . 14
238104, 237sstri 3359 . . . . . . . . . . . . 13
239238a1i 11 . . . . . . . . . . . 12
240 cnrest2 17352 . . . . . . . . . . . 12 fld TopOn fldt fld fldt fldt
241220, 236, 239, 240syl3anc 1185 . . . . . . . . . . 11 fldt fld fldt fldt
242232, 241mpbid 203 . . . . . . . . . 10 fldt fldt
243 blcntr 18445 . . . . . . . . . . . . 13
24438, 40, 49, 243syl3anc 1185 . . . . . . . . . . . 12
245244, 36syl6eleqr 2529 . . . . . . . . . . 11
246 resttopon 17227 . . . . . . . . . . . . 13 fld TopOn fldt TopOn
247219, 53, 246sylancr 646 . . . . . . . . . . . 12 fldt TopOn
248 toponuni 16994 . . . . . . . . . . . 12 fldt TopOn fldt
249247, 248syl 16 . . . . . . . . . . 11 fldt
250245, 249eleqtrd 2514 . . . . . . . . . 10 fldt
251 eqid 2438 . . . . . . . . . . 11 fldt fldt
252251cncnpi 17344 . . . . . . . . . 10 fldt fldt fldt fldt fldt
253242, 250, 252syl2anc 644 . . . . . . . . 9 fldt fldt
254 cnex 9073 . . . . . . . . . . . 12
255254prid2 3915 . . . . . . . . . . 11
256 logf1o 20464 . . . . . . . . . . . . . 14
257 f1of 5676 . . . . . . . . . . . . . 14
258256, 257ax-mp 8 . . . . . . . . . . . . 13
259 logrncn 20462 . . . . . . . . . . . . . 14
260259ssriv 3354 . . . . . . . . . . . . 13
261 fss 5601 . . . . . . . . . . . . 13
262258, 260, 261mp2an 655 . . . . . . . . . . . 12
263 fssres 5612 . . . . . . . . . . . 12
264262, 104, 263mp2an 655 . . . . . . . . . . 11
265 blcntr 18445 . . . . . . . . . . . . . 14
26637, 9, 146, 265mp3an 1280 . . . . . . . . . . . . 13
267 ovex 6108 . . . . . . . . . . . . . 14
268100dvlog2 20546 . . . . . . . . . . . . . 14
269267, 268dmmpti 5576 . . . . . . . . . . . . 13
270266, 269eleqtrri 2511 . . . . . . . . . . . 12
271 eqid 2438 . . . . . . . . . . . . 13 fldt fldt
272268fveq1i 5731 . . . . . . . . . . . . . . . . 17
273 oveq2 6091 . . . . . . . . . . . . . . . . . . . 20
2749div1i 9744 . . . . . . . . . . . . . . . . . . . 20
275273, 274syl6eq 2486 . . . . . . . . . . . . . . . . . . 19
276 eqid 2438 . . . . . . . . . . . . . . . . . . 19
277 1ex 9088 . . . . . . . . . . . . . . . . . . 19
278275, 276, 277fvmpt 5808 . . . . . . . . . . . . . . . . . 18
279266, 278ax-mp 8 . . . . . . . . . . . . . . . . 17
280272, 279eqtr2i 2459 . . . . . . . . . . . . . . . 16
281280a1i 11 . . . . . . . . . . . . . . 15
282 fvres 5747 . . . . . . . . . . . . . . . . . 18
283 fvres 5747 . . . . . . . . . . . . . . . . . . . 20
284266, 283mp1i 12 . . . . . . . . . . . . . . . . . . 19
285 log1 20482 . . . . . . . . . . . . . . . . . . 19
286284, 285syl6eq 2486 . . . . . . . . . . . . . . . . . 18
287282, 286oveq12d 6101 . . . . . . . . . . . . . . . . 17
288104sseli 3346 . . . . . . . . . . . . . . . . . . . 20
289 eldifsn 3929 . . . . . . . . . . . . . . . . . . . 20
290288, 289sylib 190 . . . . . . . . . . . . . . . . . . 19
291 logcl 20468 . . . . . . . . . . . . . . . . . . 19
292290, 291syl 16 . . . . . . . . . . . . . . . . . 18
293292subid1d 9402 . . . . . . . . . . . . . . . . 17
294287, 293eqtr2d 2471 . . . . . . . . . . . . . . . 16
295294oveq1d 6098 . . . . . . . . . . . . . . 15
296281, 295ifeq12d 3757 . . . . . . . . . . . . . 14
297296mpteq2ia 4293 . . . . . . . . . . . . 13
298271, 218, 297dvcnp 19807 . . . . . . . . . . . 12 fldt fld
299270, 298mpan2 654 . . . . . . . . . . 11 fldt fld
300255, 264, 238, 299mp3an 1280 . . . . . . . . . 10 fldt fld
301 oveq2 6091 . . . . . . . . . . . . . . 15
302301oveq2d 6099 . . . . . . . . . . . . . 14
303 ovex 6108 . . . . . . . . . . . . . 14
304302, 233, 303fvmpt 5808 . . . . . . . . . . . . 13
305245, 304syl 16 . . . . . . . . . . . 12
306 mul01 9247 . . . . . . . . . . . . . 14
307306oveq2d 6099 . . . . . . . . . . . . 13
308307, 70syl6eq 2486 . . . . . . . . . . . 12
309305, 308eqtrd 2470 . . . . . . . . . . 11
310309fveq2d 5734 . . . . . . . . . 10 fldt fld fldt fld
311300, 310syl5eleqr 2525 . . . . . . . . 9 fldt fld
312 cnpco 17333 . . . . . . . . 9 fldt fldt fldt fld fldt fld
313253, 311, 312syl2anc 644 . . . . . . . 8 fldt fld
314216, 313eqeltrrd 2513 . . . . . . 7 fldt fld
315220, 220, 223cnmptc 17696 . . . . . . . . . 10 fld fld
316220cnmptid 17695 . . . . . . . . . 10 fld fld
317220, 315, 316, 227cnmpt12f 17700 . . . . . . . . 9 fld fld
318 efcn 20361 . . . . . . . . . . 11
319218cncfcn1 18942 . . . . . . . . . . 11 fld fld
320318, 319eleqtri 2510 . . . . . . . . . 10 fld fld
321320a1i 11 . . . . . . . . 9 fld fld
322220, 317, 321cnmpt11f 17698 . . . . . . . 8 fld fld
323 eqid 2438 . . . . . . . . . 10
324189, 323fmptd 5895 . . . . . . . . 9
325324, 245ffvelrnd 5873 . . . . . . . 8
326219toponunii 16999 . . . . . . . . 9 fld
327326cncnpi 17344 . . . . . . . 8 fld fld fld fld
328322, 325, 327syl2anc 644 . . . . . . 7 fld fld
329 cnpco 17333 . . . . . . 7 fldt fld fld fld fldt fld
330314, 328, 329syl2anc 644 . . . . . 6 fldt fld
331201, 330eqeltrd 2512 . . . . 5 fldt fld
332218cnfldtop 18820 . . . . . . 7 fld
333332a1i 11 . . . . . 6 fld
334218cnfldtopn 18818 . . . . . . . . . . 11 fld
335334blopn 18532 . . . . . . . . . 10 fld
33638, 40, 50, 335syl3anc 1185 . . . . . . . . 9 fld
33736, 336syl5eqel 2522 . . . . . . . 8 fld
338 isopn3i 17148 . . . . . . . 8 fld fld fld
339332, 337, 338sylancr 646 . . . . . . 7 fld
340245, 339eleqtrrd 2515 . . . . . 6 fld
341 efcl 12687 . . . . . . . . 9
342341ad2antrr 708 . . . . . . . 8
3439, 18, 97sylancr 646 . . . . . . . . 9
344343, 60cxpcld 20601 . . . . . . . 8
345342, 344ifclda 3768 . . . . . . 7
346 eqid 2438 . . . . . . 7
347345, 346fmptd 5895 . . . . . 6
348326, 326cnprest 17355 . . . . . 6 fld fld fld fld fldt fld
349333, 53, 340, 347, 348syl22anc 1186 . . . . 5 fld fld fldt fld
350331, 349mpbird 225 . . . 4 fld fld
351326cnpresti 17354 . . . 4 fld fld fldt fld
35229, 33, 350, 351syl3anc 1185 . . 3 fldt fld
35328, 352eqeltrd 2512 . 2 fldt fld
354 simpl 445 . . . . . 6
355 rpcn 10622 . . . . . . 7
356355adantl 454 . . . . . 6
357 rpne0 10629 . . . . . . 7
358357adantl 454 . . . . . 6
359354, 356, 358divcld 9792 . . . . 5
360 addcl 9074 . . . . 5
3619, 359, 360sylancr 646 . . . 4
362361, 356cxpcld 20601 . . 3
363 oveq2 6091 . . . . 5
364363oveq2d 6099 . . . 4
365 id 21 . . . 4
366364, 365oveq12d 6101 . . 3
367 eqid 2438 . . 3 fldt fldt
368341, 362, 366, 218, 367rlimcnp3 20808 . 2 fld