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

Theorem expcnv 9819
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 8443 . . 3
2 1z 8244 . . . 4
32a1i 10 . . 3
4 nn0ex 8171 . . . . 5
54mptex 5227 . . . 4
65a1i 10 . . 3
7 0cn 7356 . . . 4
87a1i 10 . . 3
9 nnnn0 8172 . . . . . 6
10 oveq2 5038 . . . . . . 7
11 eqid 1918 . . . . . . 7
12 ovex 5054 . . . . . . 7
1310, 11, 12fvmpt 5250 . . . . . 6
149, 13syl 15 . . . . 5
15 simpr 440 . . . . . 6
1615oveq1d 5044 . . . . 5
1714, 16sylan9eqr 1972 . . . 4
18 0exp 9043 . . . . 5
1918adantl 445 . . . 4
2017, 19eqtrd 1950 . . 3
211, 3, 6, 8, 20climconst 9572 . 2
222a1i 10 . . . 4
23 expcnv.2 . . . . . . . . . . 11
2423adantr 444 . . . . . . . . . 10
25 expcnv.1 . . . . . . . . . . . 12
26 absrpcl 9437 . . . . . . . . . . . 12
2725, 26sylan 450 . . . . . . . . . . 11
28 elrp 8626 . . . . . . . . . . . 12
29 reclt1 7916 . . . . . . . . . . . 12
3028, 29sylbi 185 . . . . . . . . . . 11
3127, 30syl 15 . . . . . . . . . 10
3224, 31mpbid 199 . . . . . . . . 9
33 1re 7364 . . . . . . . . . 10
34 rpreccl 8645 . . . . . . . . . . . 12
3527, 34syl 15 . . . . . . . . . . 11
36 rpre 8629 . . . . . . . . . . 11
3735, 36syl 15 . . . . . . . . . 10
38 difrp 8653 . . . . . . . . . 10
3933, 37, 38sylancr 639 . . . . . . . . 9
4032, 39mpbid 199 . . . . . . . 8
41 rpreccl 8645 . . . . . . . 8
4240, 41syl 15 . . . . . . 7
43 rpre 8629 . . . . . . 7
4442, 43syl 15 . . . . . 6
4544recnd 7345 . . . . 5
46 divcnv 9812 . . . . 5
4745, 46syl 15 . . . 4
48 nnex 7975 . . . . . 6
4948mptex 5227 . . . . 5
5049a1i 10 . . . 4
51 oveq2 5038 . . . . . . 7
52 eqid 1918 . . . . . . 7
53 ovex 5054 . . . . . . 7
5451, 52, 53fvmpt 5250 . . . . . 6
5554adantl 445 . . . . 5
56 nndivre 8004 . . . . . 6
5744, 56sylan 450 . . . . 5
5855, 57eqeltrd 1991 . . . 4
59 oveq2 5038 . . . . . . . 8
60 eqid 1918 . . . . . . . 8
61 ovex 5054 . . . . . . . 8
6259, 60, 61fvmpt 5250 . . . . . . 7
6362adantl 445 . . . . . 6
64 nnz 8236 . . . . . . 7
65 rpexpcl 9030 . . . . . . 7
6627, 64, 65syl2an 456 . . . . . 6
6763, 66eqeltrd 1991 . . . . 5
68 rpre 8629 . . . . 5
6967, 68syl 15 . . . 4
70 nnrp 8631 . . . . . . . . . . 11
71 rpmulcl 8643 . . . . . . . . . . 11
7240, 70, 71syl2an 456 . . . . . . . . . 10
73 rpre 8629 . . . . . . . . . 10
7472, 73syl 15 . . . . . . . . 9
75 peano2re 7464 . . . . . . . . . 10
7674, 75syl 15 . . . . . . . . 9
77 rpexpcl 9030 . . . . . . . . . . 11
7835, 64, 77syl2an 456 . . . . . . . . . 10
79 rpre 8629 . . . . . . . . . 10
8078, 79syl 15 . . . . . . . . 9
81 lep1 7838 . . . . . . . . . 10
8274, 81syl 15 . . . . . . . . 9
8337adantr 444 . . . . . . . . . 10
849adantl 445 . . . . . . . . . 10
85 rpge0 8634 . . . . . . . . . . . 12
8635, 85syl 15 . . . . . . . . . . 11
8786adantr 444 . . . . . . . . . 10
88 bernneq2 9127 . . . . . . . . . 10
8983, 84, 87, 88syl3anc 1142 . . . . . . . . 9
9074, 76, 80, 82, 89letrd 7415 . . . . . . . 8
91 rpcnne0 8639 . . . . . . . . . 10
9227, 91syl 15 . . . . . . . . 9
93 exprec 9049 . . . . . . . . . 10
94933expa 1112 . . . . . . . . 9
9592, 64, 94syl2an 456 . . . . . . . 8
9690, 95breqtrd 3420 . . . . . . 7
97 elrp 8626 . . . . . . . . 9
98 elrp 8626 . . . . . . . . 9
99 lerec2 7907 . . . . . . . . 9
10097, 98, 99syl2anb 458 . . . . . . . 8
10172, 66, 100syl2anc 637 . . . . . . 7
10296, 101mpbid 199 . . . . . 6
103 rpcnne0 8639 . . . . . . . 8
10440, 103syl 15 . . . . . . 7
105 nncn 7980 . . . . . . . 8
106 nnne0 8001 . . . . . . . 8
107105, 106jca 513 . . . . . . 7
108 recdiv2 7819 . . . . . . 7
109104, 107, 108syl2an 456 . . . . . 6
110102, 109breqtrrd 3422 . . . . 5
111110, 63, 553brtr4d 3426 . . . 4
112 rpge0 8634 . . . . 5
11367, 112syl 15 . . . 4
1141, 22, 47, 50, 58, 69, 111, 113climsqz2 9626 . . 3
1152a1i 10 . . . . 5
1165a1i 10 . . . . 5
11749a1i 10 . . . . 5
1189adantl 445 . . . . . . 7
119118, 13syl 15 . . . . . 6
120 expcl 9029 . . . . . . 7
12125, 9, 120syl2an 456 . . . . . 6
122119, 121eqeltrd 1991 . . . . 5
123 absexp 9452 . . . . . . 7
12425, 9, 123syl2an 456 . . . . . 6
125119fveq2d 4765 . . . . . 6
12662adantl 445 . . . . . 6
127124, 125, 1263eqtr4rd 1961 . . . . 5
1281, 115, 116, 117, 122, 127climabs0 9601 . . . 4
129128biimpar 464 . . 3
130114, 129syldan 449 . 2
13121, 130pm2.61dane 2110 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 174   wa 357   wceq 1414   wcel 1416   wne 2035  cvv 2327   class class class wbr 3396  cfv 4046  (class class class)co 5032   cmpt 5194  cc 7255  cr 7256  cc0 7257  c1 7258   caddc 7260   cmul 7262   cle 7366   clt 7370   cmin 7487   cdiv 7489  cn 7490  cn0 7491  cz 7492  crp 7494  cexp 9012  cabs 9360   cli 9535
This theorem is referenced by:  explecnv 9820  geolim 9822  geo2lim 9826  mbfi1fseqlem6 13820  geomcau 19552
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-13 1422  ax-14 1423  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-ext 1900  ax-rep 3481  ax-sep 3491  ax-nul 3500  ax-pow 3536  ax-pr 3560  ax-un 3836  ax-inf2 6289  ax-resscn 7311  ax-1cn 7312  ax-icn 7313  ax-addcl 7314  ax-addrcl 7315  ax-mulcl 7316  ax-mulrcl 7317  ax-mulcom 7318  ax-addass 7319  ax-mulass 7320  ax-distr 7321  ax-i2m1 7322  ax-1ne0 7323  ax-1rid 7324  ax-rnegex 7325  ax-rrecex 7326  ax-cnre 7327  ax-pre-lttri 7328  ax-pre-lttrn 7329  ax-pre-ltadd 7330  ax-pre-mulgt0 7331  ax-pre-sup 7332
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1309  df-ex 1336  df-sb 1591  df-eu 1818  df-mo 1819  df-clab 1906  df-cleq 1911  df-clel 1914  df-ne 2037  df-nel 2038  df-ral 2131  df-rex 2132  df-reu 2133  df-rab 2134  df-v 2329  df-sbc 2496  df-csb 2578  df-dif 2640  df-un 2642  df-in 2644  df-ss 2648  df-pss 2650  df-nul 2908  df-if 3015  df-pw 3075  df-sn 3092  df-pr 3093  df-tp 3094  df-op 3095  df-uni 3247  df-iun 3320  df-br 3397  df-opab 3450  df-tr 3465  df-eprel 3646  df-id 3650  df-po 3655  df-so 3669  df-fr 3689  df-we 3705  df-ord 3721  df-on 3722  df-lim 3723  df-suc 3724  df-om 4001  df-xp 4048  df-rel 4049  df-cnv 4050  df-co 4051  df-dm 4052  df-rn 4053  df-res 4054  df-ima 4055  df-fun 4056  df-fn 4057  df-f 4058  df-f1 4059  df-fo 4060  df-f1o 4061  df-fv 4062  df-ov 5034  df-oprab 5035  df-mpt 5196  df-mpt2 5197  df-1st 5333  df-2nd 5334  df-iota 5444  df-rdg 5535  df-er 5710  df-map 5802  df-pm 5803  df-en 5869  df-dom 5870  df-sdom 5871  df-riota 6022  df-sup 6201  df-pnf 7371  df-mnf 7372  df-xr 7373  df-ltxr 7374  df-le 7375  df-sub 7506  df-neg 7508  df-div 7734  df-n 7974  df-2 8020  df-3 8021  df-n0 8166  df-z 8217  df-uz 8411  df-q 8497  df-rp 8625  df-fl 8860  df-seq 8959  df-exp 9013  df-cj 9265  df-re 9266  df-im 9267  df-sqr 9361  df-abs 9362  df-clim 9538  df-rlim 9539
Copyright terms: Public domain