HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem expcnv 10644
Description: A sequence of powers of a complex number with absolute value smaller than 1 converges to zero. (The proof was shortened by Mario Carneiro, 26-Apr-2014.)
Hypotheses
Ref Expression
expcnv.1
expcnv.2
Assertion
Ref Expression
expcnv
Distinct variable group:   ,
Allowed substitution hint:   ()

Proof of Theorem expcnv
StepHypRef Expression
1 nnuz 9254 . . 3
2 1z 9054 . . . 4
32a1i 10 . . 3
4 nn0ex 8980 . . . . 5
54mptex 5492 . . . 4
65a1i 10 . . 3
7 0cn 8164 . . . 4
87a1i 10 . . 3
9 nnnn0 8981 . . . . . 6
10 oveq2 5302 . . . . . . 7
11 eqid 2090 . . . . . . 7
12 ovex 5318 . . . . . . 7
1310, 11, 12fvmpt 5516 . . . . . 6
149, 13syl 15 . . . . 5
15 simpr 440 . . . . . 6
1615oveq1d 5308 . . . . 5
1714, 16sylan9eqr 2144 . . . 4
18 0exp 9862 . . . . 5
1918adantl 445 . . . 4
2017, 19eqtrd 2122 . . 3
211, 3, 6, 8, 20climconst 10393 . 2
222a1i 10 . . . 4
23 expcnv.2 . . . . . . . . . . 11
2423adantr 444 . . . . . . . . . 10
25 expcnv.1 . . . . . . . . . . . 12
26 absrpcl 10260 . . . . . . . . . . . 12
2725, 26sylan 450 . . . . . . . . . . 11
28 elrp 9441 . . . . . . . . . . . 12
29 reclt1 8724 . . . . . . . . . . . 12
3028, 29sylbi 185 . . . . . . . . . . 11
3127, 30syl 15 . . . . . . . . . 10
3224, 31mpbid 199 . . . . . . . . 9
33 1re 8172 . . . . . . . . . 10
34 rpreccl 9460 . . . . . . . . . . . 12
3527, 34syl 15 . . . . . . . . . . 11
36 rpre 9444 . . . . . . . . . . 11
3735, 36syl 15 . . . . . . . . . 10
38 difrp 9468 . . . . . . . . . 10
3933, 37, 38sylancr 639 . . . . . . . . 9
4032, 39mpbid 199 . . . . . . . 8
41 rpreccl 9460 . . . . . . . 8
4240, 41syl 15 . . . . . . 7
43 rpre 9444 . . . . . . 7
4442, 43syl 15 . . . . . 6
4544recnd 8153 . . . . 5
46 divcnv 10635 . . . . 5
4745, 46syl 15 . . . 4
48 nnex 8787 . . . . . 6
4948mptex 5492 . . . . 5
5049a1i 10 . . . 4
51 oveq2 5302 . . . . . . 7
52 eqid 2090 . . . . . . 7
53 ovex 5318 . . . . . . 7
5451, 52, 53fvmpt 5516 . . . . . 6
5554adantl 445 . . . . 5
56 nndivre 8813 . . . . . 6
5744, 56sylan 450 . . . . 5
5855, 57eqeltrd 2163 . . . 4
59 oveq2 5302 . . . . . . . 8
60 eqid 2090 . . . . . . . 8
61 ovex 5318 . . . . . . . 8
6259, 60, 61fvmpt 5516 . . . . . . 7
6362adantl 445 . . . . . 6
64 nnz 9046 . . . . . . 7
65 rpexpcl 9847 . . . . . . 7
6627, 64, 65syl2an 456 . . . . . 6
6763, 66eqeltrd 2163 . . . . 5
68 rpre 9444 . . . . 5
6967, 68syl 15 . . . 4
70 nnrp 9446 . . . . . . . . . . 11
71 rpmulcl 9458 . . . . . . . . . . 11
7240, 70, 71syl2an 456 . . . . . . . . . 10
73 rpre 9444 . . . . . . . . . 10
7472, 73syl 15 . . . . . . . . 9
75 peano2re 8272 . . . . . . . . . 10
7674, 75syl 15 . . . . . . . . 9
77 rpexpcl 9847 . . . . . . . . . . 11
7835, 64, 77syl2an 456 . . . . . . . . . 10
79 rpre 9444 . . . . . . . . . 10
8078, 79syl 15 . . . . . . . . 9
81 lep1 8646 . . . . . . . . . 10
8274, 81syl 15 . . . . . . . . 9
8337adantr 444 . . . . . . . . . 10
849adantl 445 . . . . . . . . . 10
85 rpge0 9449 . . . . . . . . . . . 12
8635, 85syl 15 . . . . . . . . . . 11
8786adantr 444 . . . . . . . . . 10
88 bernneq2 9946 . . . . . . . . . 10
8983, 84, 87, 88syl3anc 1145 . . . . . . . . 9
9074, 76, 80, 82, 89letrd 8223 . . . . . . . 8
91 rpcnne0 9454 . . . . . . . . . 10
9227, 91syl 15 . . . . . . . . 9
93 exprec 9868 . . . . . . . . . 10
94933expa 1115 . . . . . . . . 9
9592, 64, 94syl2an 456 . . . . . . . 8
9690, 95breqtrd 3615 . . . . . . 7
97 elrp 9441 . . . . . . . . 9
98 elrp 9441 . . . . . . . . 9
99 lerec2 8715 . . . . . . . . 9
10097, 98, 99syl2anb 458 . . . . . . . 8
10172, 66, 100syl2anc 637 . . . . . . 7
10296, 101mpbid 199 . . . . . 6
103 rpcnne0 9454 . . . . . . . 8
10440, 103syl 15 . . . . . . 7
105 nncn 8789 . . . . . . . 8
106 nnne0 8810 . . . . . . . 8
107105, 106jca 513 . . . . . . 7
108 recdiv2 8627 . . . . . . 7
109104, 107, 108syl2an 456 . . . . . 6
110102, 109breqtrrd 3617 . . . . 5
111110, 63, 553brtr4d 3621 . . . 4
112 rpge0 9449 . . . . 5
11367, 112syl 15 . . . 4
1141, 22, 47, 50, 58, 69, 111, 113climsqz2 10447 . . 3
1152a1i 10 . . . . 5
1165a1i 10 . . . . 5
11749a1i 10 . . . . 5
1189adantl 445 . . . . . . 7
119118, 13syl 15 . . . . . 6
120 expcl 9846 . . . . . . 7
12125, 9, 120syl2an 456 . . . . . 6
122119, 121eqeltrd 2163 . . . . 5
123 absexp 10275 . . . . . . 7
12425, 9, 123syl2an 456 . . . . . 6
125119fveq2d 4996 . . . . . 6
12662adantl 445 . . . . . 6
127124, 125, 1263eqtr4rd 2133 . . . . 5
1281, 115, 116, 117, 122, 127climabs0 10422 . . . 4
129128biimpar 464 . . 3
130114, 129syldan 449 . 2
13121, 130pm2.61dane 2282 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 174   wa 357   wceq 1531   wcel 1533   wne 2207  cvv 2500   class class class wbr 3591  cfv 4261  (class class class)co 5296   cmpt 5459  cc 8059  cr 8060  cc0 8061  c1 8062   caddc 8064   cmul 8066   cle 8174   clt 8178   cmin 8295   cdiv 8297  cn 8298  cn0 8299  cz 8300  crp 8302  cexp 9829  cabs 10183   cli 10356
This theorem is referenced by:  explecnv  10645  geolim  10647  geo2lim  10651  mbfi1fseqlem6  14903  geomcau  21164
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-13 1538  ax-14 1539  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-rep 3677  ax-sep 3687  ax-nul 3696  ax-pow 3732  ax-pr 3756  ax-un 4049  ax-cnex 8116  ax-resscn 8117  ax-1cn 8118  ax-icn 8119  ax-addcl 8120  ax-addrcl 8121  ax-mulcl 8122  ax-mulrcl 8123  ax-mulcom 8124  ax-addass 8125  ax-mulass 8126  ax-distr 8127  ax-i2m1 8128  ax-1ne0 8129  ax-1rid 8130  ax-rnegex 8131  ax-rrecex 8132  ax-cnre 8133  ax-pre-lttri 8134  ax-pre-lttrn 8135  ax-pre-ltadd 8136  ax-pre-mulgt0 8137  ax-pre-sup 8138
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1264  df-ex 1451  df-sb 1751  df-eu 1984  df-mo 1985  df-clab 2078  df-cleq 2083  df-clel 2086  df-ne 2209  df-nel 2210  df-ral 2303  df-rex 2304  df-reu 2305  df-rab 2306  df-v 2502  df-sbc 2669  df-csb 2751  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-pss 2823  df-nul 3086  df-if 3195  df-pw 3256  df-sn 3274  df-pr 3275  df-tp 3276  df-op 3277  df-uni 3435  df-iun 3511  df-br 3592  df-opab 3645  df-tr 3660  df-eprel 3844  df-id 3848  df-po 3853  df-so 3854  df-fr 3891  df-we 3893  df-ord 3934  df-on 3935  df-lim 3936  df-suc 3937  df-om 4216  df-xp 4263  df-rel 4264  df-cnv 4265  df-co 4266  df-dm 4267  df-rn 4268  df-res 4269  df-ima 4270  df-fun 4271  df-fn 4272  df-f 4273  df-f1 4274  df-fo 4275  df-f1o 4276  df-fv 4277  df-ov 5298  df-oprab 5299  df-mpt 5461  df-mpt2 5462  df-2nd 5614  df-iota 5740  df-recs 5814  df-rdg 5849  df-er 6076  df-pm 6172  df-en 6249  df-dom 6250  df-sdom 6251  df-riota 6415  df-sup 6607  df-pnf 8179  df-mnf 8180  df-xr 8181  df-ltxr 8182  df-le 8183  df-sub 8314  df-neg 8316  df-div 8542  df-n 8782  df-2 8829  df-3 8830  df-n0 8975  df-z 9026  df-uz 9222  df-rp 9440  df-fl 9675  df-seq 9775  df-exp 9830  df-cj 10086  df-re 10087  df-im 10088  df-sqr 10184  df-abs 10185  df-clim 10359  df-rlim 10360
Copyright terms: Public domain