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

Theorem expcnv 9519
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 8180 . . 3
2 1z 8056 . . . 4
32a1i 10 . . 3
4 nn0ex 7989 . . . . 5
54mptex 5137 . . . 4
65a1i 10 . . 3
7 0cn 7205 . . . 4
87a1i 10 . . 3
9 nnnn0 7990 . . . . . 6
10 oveq2 4950 . . . . . . 7
11 eqid 1917 . . . . . . 7
12 ovex 4966 . . . . . . 7
1310, 11, 12fvmpt 5156 . . . . . 6
149, 13syl 14 . . . . 5
15 simpr 439 . . . . . 6
1615oveq1d 4956 . . . . 5
1714, 16sylan9eqr 1971 . . . 4
18 0exp 8770 . . . . 5
1918adantl 444 . . . 4
2017, 19eqtrd 1949 . . 3
211, 3, 6, 8, 20climconst 9283 . 2
222a1i 10 . . . 4
237a1i 10 . . . 4
24 expcnv.2 . . . . . . . . . . 11
2524adantr 443 . . . . . . . . . 10
26 expcnv.1 . . . . . . . . . . . 12
27 absrpcl 9154 . . . . . . . . . . . 12
2826, 27sylan 449 . . . . . . . . . . 11
29 elrp 8357 . . . . . . . . . . . 12
30 reclt1 7756 . . . . . . . . . . . 12
3129, 30sylbi 184 . . . . . . . . . . 11
3228, 31syl 14 . . . . . . . . . 10
3325, 32mpbid 198 . . . . . . . . 9
34 1re 7213 . . . . . . . . . 10
35 rpreccl 8376 . . . . . . . . . . . 12
3628, 35syl 14 . . . . . . . . . . 11
37 rpre 8360 . . . . . . . . . . 11
3836, 37syl 14 . . . . . . . . . 10
39 difrp 8384 . . . . . . . . . 10
4034, 38, 39sylancr 638 . . . . . . . . 9
4133, 40mpbid 198 . . . . . . . 8
42 rpreccl 8376 . . . . . . . 8
4341, 42syl 14 . . . . . . 7
44 rpre 8360 . . . . . . 7
4543, 44syl 14 . . . . . 6
4645recnd 7195 . . . . 5
47 divcnv 9513 . . . . 5
4846, 47syl 14 . . . 4
49 nnex 7815 . . . . . 6
5049mptex 5137 . . . . 5
5150a1i 10 . . . 4
52 oveq2 4950 . . . . . . 7
53 eqid 1917 . . . . . . 7
54 ovex 4966 . . . . . . 7
5552, 53, 54fvmpt 5156 . . . . . 6
5655adantl 444 . . . . 5
57 nndivre 7844 . . . . . 6
5845, 57sylan 449 . . . . 5
5956, 58eqeltrd 1990 . . . 4
60 oveq2 4950 . . . . . . . 8
61 eqid 1917 . . . . . . . 8
62 ovex 4966 . . . . . . . 8
6360, 61, 62fvmpt 5156 . . . . . . 7
6463adantl 444 . . . . . 6
65 nnz 8048 . . . . . . 7
66 rpexpcl 8758 . . . . . . 7
6728, 65, 66syl2an 455 . . . . . 6
6864, 67eqeltrd 1990 . . . . 5
69 rpre 8360 . . . . 5
7068, 69syl 14 . . . 4
71 nnrp 8362 . . . . . . . . . . 11
72 rpmulcl 8374 . . . . . . . . . . 11
7341, 71, 72syl2an 455 . . . . . . . . . 10
74 rpre 8360 . . . . . . . . . 10
7573, 74syl 14 . . . . . . . . 9
76 peano2re 7308 . . . . . . . . . 10
7775, 76syl 14 . . . . . . . . 9
78 rpexpcl 8758 . . . . . . . . . . 11
7936, 65, 78syl2an 455 . . . . . . . . . 10
80 rpre 8360 . . . . . . . . . 10
8179, 80syl 14 . . . . . . . . 9
82 lep1 7678 . . . . . . . . . 10
8375, 82syl 14 . . . . . . . . 9
8438adantr 443 . . . . . . . . . 10
859adantl 444 . . . . . . . . . 10
86 rpge0 8365 . . . . . . . . . . . 12
8736, 86syl 14 . . . . . . . . . . 11
8887adantr 443 . . . . . . . . . 10
89 bernneq2 8853 . . . . . . . . . 10
9084, 85, 88, 89syl3anc 1141 . . . . . . . . 9
9175, 77, 81, 83, 90letrd 7260 . . . . . . . 8
92 rpcnne0 8370 . . . . . . . . . 10
9328, 92syl 14 . . . . . . . . 9
94 exprec 8776 . . . . . . . . . 10
95943expa 1111 . . . . . . . . 9
9693, 65, 95syl2an 455 . . . . . . . 8
9791, 96breqtrd 3382 . . . . . . 7
98 elrp 8357 . . . . . . . . 9
99 elrp 8357 . . . . . . . . 9
100 lerec2 7747 . . . . . . . . 9
10198, 99, 100syl2anb 457 . . . . . . . 8
10273, 67, 101syl2anc 636 . . . . . . 7
10397, 102mpbid 198 . . . . . 6
104 rpcnne0 8370 . . . . . . . 8
10541, 104syl 14 . . . . . . 7
106 nncn 7820 . . . . . . . 8
107 nnne0 7841 . . . . . . . 8
108106, 107jca 512 . . . . . . 7
109 recdiv2 7660 . . . . . . 7
110105, 108, 109syl2an 455 . . . . . 6
111103, 110breqtrrd 3384 . . . . 5
112111, 64, 563brtr4d 3388 . . . 4
113 rpge0 8365 . . . . 5
11468, 113syl 14 . . . 4
1151, 22, 23, 48, 51, 59, 70, 112, 114climsqz2 9337 . . 3
1162a1i 10 . . . . 5
1175a1i 10 . . . . 5
11850a1i 10 . . . . 5
1199adantl 444 . . . . . . 7
120119, 13syl 14 . . . . . 6
121 expcl 8757 . . . . . . 7
12226, 9, 121syl2an 455 . . . . . 6
123120, 122eqeltrd 1990 . . . . 5
124 absexp 9169 . . . . . . 7
12526, 9, 124syl2an 455 . . . . . 6
126120fveq2d 4694 . . . . . 6
12763adantl 444 . . . . . 6
128125, 126, 1273eqtr4rd 1960 . . . . 5
1291, 116, 117, 118, 123, 128climabs0 9312 . . . 4
130129biimpar 463 . . 3
131115, 130syldan 448 . 2
13221, 131pm2.61dane 2108 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 173   wa 356   wceq 1413   wcel 1415   wne 2034  cvv 2322   class class class wbr 3358  cfv 4007  (class class class)co 4944   cmpt 5104  cc 7105  cr 7106  cc0 7107  c1 7108   caddc 7110   cmul 7112   cle 7215   clt 7219   cmin 7330   cdiv 7332  cn 7333  cn0 7334  cz 7335  crp 7337  cexp 8740  cabs 9077   cli 9246
This theorem is referenced by:  explecnv 9520  geolim 9522  geo2lim 9526  mbfi1fseqlem6 12921  geomcau 18193
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-13 1421  ax-14 1422  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-ext 1899  ax-rep 3444  ax-sep 3454  ax-nul 3463  ax-pow 3499  ax-pr 3523  ax-un 3797  ax-inf2 6154  ax-resscn 7161  ax-1cn 7162  ax-icn 7163  ax-addcl 7164  ax-addrcl 7165  ax-mulcl 7166  ax-mulrcl 7167  ax-mulcom 7168  ax-addass 7169  ax-mulass 7170  ax-distr 7171  ax-i2m1 7172  ax-1ne0 7173  ax-1rid 7174  ax-rnegex 7175  ax-rrecex 7176  ax-cnre 7177  ax-pre-lttri 7178  ax-pre-lttrn 7179  ax-pre-ltadd 7180  ax-pre-mulgt0 7181  ax-pre-sup 7182
This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-3or 899  df-3an 900  df-tru 1308  df-ex 1335  df-sb 1590  df-eu 1817  df-mo 1818  df-clab 1905  df-cleq 1910  df-clel 1913  df-ne 2036  df-nel 2037  df-ral 2129  df-rex 2130  df-reu 2131  df-rab 2132  df-v 2324  df-sbc 2491  df-csb 2573  df-dif 2635  df-un 2637  df-in 2639  df-ss 2641  df-pss 2643  df-nul 2899  df-if 3004  df-pw 3062  df-sn 3079  df-pr 3080  df-tp 3081  df-op 3082  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 3650  df-we 3666  df-ord 3682  df-on 3683  df-lim 3684  df-suc 3685  df-om 3962  df-xp 4009  df-rel 4010  df-cnv 4011  df-co 4012  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fun 4017  df-fn 4018  df-f 4019  df-f1 4020  df-fo 4021  df-f1o 4022  df-fv 4023  df-ov 4946  df-oprab 4947  df-mpt 5106  df-mpt2 5107  df-1st 5231  df-2nd 5232  df-iota 5336  df-rdg 5424  df-er 5598  df-map 5690  df-pm 5691  df-en 5750  df-dom 5751  df-sdom 5752  df-riota 5896  df-sup 6075  df-pnf 7220  df-mnf 7221  df-xr 7222  df-ltxr 7223  df-le 7224  df-sub 7349  df-neg 7351  df-div 7575  df-n 7814  df-2 7860  df-3 7861  df-n0 7984  df-z 8029  df-uz 8149  df-q 8231  df-rp 8356  df-fl 8595  df-seq 8688  df-exp 8741  df-cj 8984  df-re 8985  df-im 8986  df-sqr 9078  df-abs 9079  df-clim 9249  df-rlim 9250
Copyright terms: Public domain