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

Theorem expcnv 9402
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 8078 . . 3
2 1z 7954 . . . 4
32a1i 10 . . 3
4 nn0ex 7888 . . . . 5
54mptex 5093 . . . 4
65a1i 10 . . 3
7 0cn 7104 . . . 4
87a1i 10 . . 3
9 nnnn0 7889 . . . . . 6
10 oveq2 4930 . . . . . . 7
11 eqid 1929 . . . . . . 7
12 ovex 4946 . . . . . . 7
1310, 11, 12fvmpt 5110 . . . . . 6
149, 13syl 14 . . . . 5
15 simpr 444 . . . . . 6
1615oveq1d 4936 . . . . 5
1714, 16sylan9eqr 1983 . . . 4
18 0exp 8666 . . . . 5
1918adantl 449 . . . 4
2017, 19eqtrd 1961 . . 3
211, 3, 6, 8, 20climconst 9170 . 2
222a1i 10 . . . 4
237a1i 10 . . . 4
24 expcnv.2 . . . . . . . . . . 11
2524adantr 448 . . . . . . . . . 10
26 expcnv.1 . . . . . . . . . . . 12
27 absrpcl 9041 . . . . . . . . . . . 12
2826, 27sylan 454 . . . . . . . . . . 11
29 elrp 8255 . . . . . . . . . . . 12
30 reclt1 7655 . . . . . . . . . . . 12
3129, 30sylbi 185 . . . . . . . . . . 11
3228, 31syl 14 . . . . . . . . . 10
3325, 32mpbid 199 . . . . . . . . 9
34 1re 7112 . . . . . . . . . 10
35 rpreccl 8274 . . . . . . . . . . . 12
3628, 35syl 14 . . . . . . . . . . 11
37 rpre 8258 . . . . . . . . . . 11
3836, 37syl 14 . . . . . . . . . 10
39 difrp 8282 . . . . . . . . . 10
4034, 38, 39sylancr 643 . . . . . . . . 9
4133, 40mpbid 199 . . . . . . . 8
42 rpreccl 8274 . . . . . . . 8
4341, 42syl 14 . . . . . . 7
44 rpre 8258 . . . . . . 7
4543, 44syl 14 . . . . . 6
4645recnd 7094 . . . . 5
47 divcnv 9396 . . . . 5
4846, 47syl 14 . . . 4
49 nnex 7714 . . . . . 6
5049mptex 5093 . . . . 5
5150a1i 10 . . . 4
52 oveq2 4930 . . . . . . 7
53 eqid 1929 . . . . . . 7
54 ovex 4946 . . . . . . 7
5552, 53, 54fvmpt 5110 . . . . . 6
5655adantl 449 . . . . 5
57 nndivre 7743 . . . . . 6
5845, 57sylan 454 . . . . 5
5956, 58eqeltrd 2002 . . . 4
60 oveq2 4930 . . . . . . . 8
61 eqid 1929 . . . . . . . 8
62 ovex 4946 . . . . . . . 8
6360, 61, 62fvmpt 5110 . . . . . . 7
6463adantl 449 . . . . . 6
65 nnz 7946 . . . . . . 7
66 rpexpcl 8654 . . . . . . 7
6728, 65, 66syl2an 460 . . . . . 6
6864, 67eqeltrd 2002 . . . . 5
69 rpre 8258 . . . . 5
7068, 69syl 14 . . . 4
71 nnrp 8260 . . . . . . . . . . 11
72 rpmulcl 8272 . . . . . . . . . . 11
7341, 71, 72syl2an 460 . . . . . . . . . 10
74 rpre 8258 . . . . . . . . . 10
7573, 74syl 14 . . . . . . . . 9
76 peano2re 7207 . . . . . . . . . 10
7775, 76syl 14 . . . . . . . . 9
78 rpexpcl 8654 . . . . . . . . . . 11
7936, 65, 78syl2an 460 . . . . . . . . . 10
80 rpre 8258 . . . . . . . . . 10
8179, 80syl 14 . . . . . . . . 9
82 lep1 7577 . . . . . . . . . 10
8375, 82syl 14 . . . . . . . . 9
8438adantr 448 . . . . . . . . . 10
859adantl 449 . . . . . . . . . 10
86 rpge0 8263 . . . . . . . . . . . 12
8736, 86syl 14 . . . . . . . . . . 11
8887adantr 448 . . . . . . . . . 10
89 bernneq2 8750 . . . . . . . . . 10
9084, 85, 88, 89syl3anc 1153 . . . . . . . . 9
9175, 77, 81, 83, 90letrd 7159 . . . . . . . 8
92 rpcnne0 8268 . . . . . . . . . 10
9328, 92syl 14 . . . . . . . . 9
94 exprec 8672 . . . . . . . . . 10
95943expa 1123 . . . . . . . . 9
9693, 65, 95syl2an 460 . . . . . . . 8
9791, 96breqtrd 3382 . . . . . . 7
98 elrp 8255 . . . . . . . . 9
99 elrp 8255 . . . . . . . . 9
100 lerec2 7646 . . . . . . . . 9
10198, 99, 100syl2anb 462 . . . . . . . 8
10273, 67, 101syl2anc 641 . . . . . . 7
10397, 102mpbid 199 . . . . . 6
104 rpcnne0 8268 . . . . . . . 8
10541, 104syl 14 . . . . . . 7
106 nncn 7719 . . . . . . . 8
107 nnne0 7740 . . . . . . . 8
108106, 107jca 517 . . . . . . 7
109 recdiv2 7559 . . . . . . 7
110105, 108, 109syl2an 460 . . . . . 6
111103, 110breqtrrd 3384 . . . . 5
112111, 64, 563brtr4d 3388 . . . 4
113 rpge0 8263 . . . . 5
11468, 113syl 14 . . . 4
1151, 22, 23, 48, 51, 59, 70, 112, 114climsqz2 9224 . . 3
1162a1i 10 . . . . 5
1175a1i 10 . . . . 5
11850a1i 10 . . . . 5
1199adantl 449 . . . . . . 7
120119, 13syl 14 . . . . . 6
121 expcl 8653 . . . . . . 7
12226, 9, 121syl2an 460 . . . . . 6
123120, 122eqeltrd 2002 . . . . 5
124 absexp 9056 . . . . . . 7
12526, 9, 124syl2an 460 . . . . . 6
126120fveq2d 4676 . . . . . 6
12763adantl 449 . . . . . 6
128125, 126, 1273eqtr4rd 1972 . . . . 5
1291, 116, 117, 118, 123, 128climabs0 9199 . . . 4
130129biimpar 468 . . 3
131115, 130syldan 453 . 2
13221, 131pm2.61dane 2121 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 174   wa 360   wceq 1425   wcel 1427   wne 2047  cvv 2335   class class class wbr 3358  cfv 4003  (class class class)co 4924   cmpt 5061  cc 7004  cr 7005  cc0 7006  c1 7007   caddc 7009   cmul 7011   cle 7114   clt 7118   cmin 7229   cdiv 7231  cn 7232  cn0 7233  cz 7234  crp 7236  cexp 8636  cabs 8964   cli 9133
This theorem is referenced by:  explecnv 9403  geolim 9405  geo2lim 9409  mbfi1fseqlem6 12314  geomcau 17277
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-13 1433  ax-14 1434  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-ext 1911  ax-rep 3444  ax-sep 3454  ax-nul 3463  ax-pow 3499  ax-pr 3523  ax-un 3795  ax-inf2 6078  ax-resscn 7060  ax-1cn 7061  ax-icn 7062  ax-addcl 7063  ax-addrcl 7064  ax-mulcl 7065  ax-mulrcl 7066  ax-mulcom 7067  ax-addass 7068  ax-mulass 7069  ax-distr 7070  ax-i2m1 7071  ax-1ne0 7072  ax-1rid 7073  ax-rnegex 7074  ax-rrecex 7075  ax-cnre 7076  ax-pre-lttri 7077  ax-pre-lttrn 7078  ax-pre-ltadd 7079  ax-pre-mulgt0 7080  ax-pre-sup 7081
This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-3or 913  df-3an 914  df-tru 1320  df-ex 1347  df-sb 1602  df-eu 1829  df-mo 1830  df-clab 1917  df-cleq 1922  df-clel 1925  df-ne 2049  df-nel 2050  df-ral 2142  df-rex 2143  df-reu 2144  df-rab 2145  df-v 2337  df-sbc 2502  df-csb 2577  df-dif 2637  df-un 2639  df-in 2641  df-ss 2643  df-pss 2645  df-nul 2900  df-if 3005  df-pw 3063  df-sn 3080  df-pr 3081  df-tp 3082  df-op 3083  df-uni 3214  df-iun 3286  df-br 3359  df-opab 3413  df-tr 3428  df-eprel 3608  df-id 3611  df-po 3616  df-so 3630  df-fr 3649  df-we 3665  df-ord 3681  df-on 3682  df-lim 3683  df-suc 3684  df-om 3958  df-xp 4005  df-rel 4006  df-cnv 4007  df-co 4008  df-dm 4009  df-rn 4010  df-res 4011  df-ima 4012  df-fun 4013  df-fn 4014  df-f 4015  df-f1 4016  df-fo 4017  df-f1o 4018  df-fv 4019  df-ov 4926  df-oprab 4927  df-mpt 5063  df-mpt2 5064  df-1st 5173  df-2nd 5174  df-iota 5277  df-rdg 5363  df-er 5537  df-map 5625  df-pm 5626  df-en 5682  df-dom 5683  df-sdom 5684  df-riota 5825  df-sup 5999  df-pnf 7119  df-mnf 7120  df-xr 7121  df-ltxr 7122  df-le 7123  df-sub 7248  df-neg 7250  df-div 7474  df-n 7713  df-2 7759  df-3 7760  df-n0 7883  df-z 7927  df-uz 8047  df-q 8129  df-rp 8254  df-fl 8492  df-seq 8585  df-exp 8637  df-cj 8871  df-re 8872  df-im 8873  df-sqr 8965  df-abs 8966  df-clim 9136  df-rlim 9137
Copyright terms: Public domain