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

Theorem expcnv 9585
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 8245 . . 3
2 1z 8121 . . . 4
32a1i 10 . . 3
4 nn0ex 8054 . . . . 5
54mptex 5173 . . . 4
65a1i 10 . . 3
7 0cn 7268 . . . 4
87a1i 10 . . 3
9 nnnn0 8055 . . . . . 6
10 oveq2 4985 . . . . . . 7
11 eqid 1918 . . . . . . 7
12 ovex 5001 . . . . . . 7
1310, 11, 12fvmpt 5192 . . . . . 6
149, 13syl 15 . . . . 5
15 simpr 440 . . . . . 6
1615oveq1d 4991 . . . . 5
1714, 16sylan9eqr 1972 . . . 4
18 0exp 8836 . . . . 5
1918adantl 445 . . . 4
2017, 19eqtrd 1950 . . 3
211, 3, 6, 8, 20climconst 9349 . 2
222a1i 10 . . . 4
237a1i 10 . . . 4
24 expcnv.2 . . . . . . . . . . 11
2524adantr 444 . . . . . . . . . 10
26 expcnv.1 . . . . . . . . . . . 12
27 absrpcl 9220 . . . . . . . . . . . 12
2826, 27sylan 450 . . . . . . . . . . 11
29 elrp 8422 . . . . . . . . . . . 12
30 reclt1 7819 . . . . . . . . . . . 12
3129, 30sylbi 185 . . . . . . . . . . 11
3228, 31syl 15 . . . . . . . . . 10
3325, 32mpbid 199 . . . . . . . . 9
34 1re 7276 . . . . . . . . . 10
35 rpreccl 8441 . . . . . . . . . . . 12
3628, 35syl 15 . . . . . . . . . . 11
37 rpre 8425 . . . . . . . . . . 11
3836, 37syl 15 . . . . . . . . . 10
39 difrp 8449 . . . . . . . . . 10
4034, 38, 39sylancr 639 . . . . . . . . 9
4133, 40mpbid 199 . . . . . . . 8
42 rpreccl 8441 . . . . . . . 8
4341, 42syl 15 . . . . . . 7
44 rpre 8425 . . . . . . 7
4543, 44syl 15 . . . . . 6
4645recnd 7258 . . . . 5
47 divcnv 9579 . . . . 5
4846, 47syl 15 . . . 4
49 nnex 7878 . . . . . 6
5049mptex 5173 . . . . 5
5150a1i 10 . . . 4
52 oveq2 4985 . . . . . . 7
53 eqid 1918 . . . . . . 7
54 ovex 5001 . . . . . . 7
5552, 53, 54fvmpt 5192 . . . . . 6
5655adantl 445 . . . . 5
57 nndivre 7907 . . . . . 6
5845, 57sylan 450 . . . . 5
5956, 58eqeltrd 1991 . . . 4
60 oveq2 4985 . . . . . . . 8
61 eqid 1918 . . . . . . . 8
62 ovex 5001 . . . . . . . 8
6360, 61, 62fvmpt 5192 . . . . . . 7
6463adantl 445 . . . . . 6
65 nnz 8113 . . . . . . 7
66 rpexpcl 8824 . . . . . . 7
6728, 65, 66syl2an 456 . . . . . 6
6864, 67eqeltrd 1991 . . . . 5
69 rpre 8425 . . . . 5
7068, 69syl 15 . . . 4
71 nnrp 8427 . . . . . . . . . . 11
72 rpmulcl 8439 . . . . . . . . . . 11
7341, 71, 72syl2an 456 . . . . . . . . . 10
74 rpre 8425 . . . . . . . . . 10
7573, 74syl 15 . . . . . . . . 9
76 peano2re 7371 . . . . . . . . . 10
7775, 76syl 15 . . . . . . . . 9
78 rpexpcl 8824 . . . . . . . . . . 11
7936, 65, 78syl2an 456 . . . . . . . . . 10
80 rpre 8425 . . . . . . . . . 10
8179, 80syl 15 . . . . . . . . 9
82 lep1 7741 . . . . . . . . . 10
8375, 82syl 15 . . . . . . . . 9
8438adantr 444 . . . . . . . . . 10
859adantl 445 . . . . . . . . . 10
86 rpge0 8430 . . . . . . . . . . . 12
8736, 86syl 15 . . . . . . . . . . 11
8887adantr 444 . . . . . . . . . 10
89 bernneq2 8919 . . . . . . . . . 10
9084, 85, 88, 89syl3anc 1142 . . . . . . . . 9
9175, 77, 81, 83, 90letrd 7323 . . . . . . . 8
92 rpcnne0 8435 . . . . . . . . . 10
9328, 92syl 15 . . . . . . . . 9
94 exprec 8842 . . . . . . . . . 10
95943expa 1112 . . . . . . . . 9
9693, 65, 95syl2an 456 . . . . . . . 8
9791, 96breqtrd 3394 . . . . . . 7
98 elrp 8422 . . . . . . . . 9
99 elrp 8422 . . . . . . . . 9
100 lerec2 7810 . . . . . . . . 9
10198, 99, 100syl2anb 458 . . . . . . . 8
10273, 67, 101syl2anc 637 . . . . . . 7
10397, 102mpbid 199 . . . . . 6
104 rpcnne0 8435 . . . . . . . 8
10541, 104syl 15 . . . . . . 7
106 nncn 7883 . . . . . . . 8
107 nnne0 7904 . . . . . . . 8
108106, 107jca 513 . . . . . . 7
109 recdiv2 7723 . . . . . . 7
110105, 108, 109syl2an 456 . . . . . 6
111103, 110breqtrrd 3396 . . . . 5
112111, 64, 563brtr4d 3400 . . . 4
113 rpge0 8430 . . . . 5
11468, 113syl 15 . . . 4
1151, 22, 23, 48, 51, 59, 70, 112, 114climsqz2 9403 . . 3
1162a1i 10 . . . . 5
1175a1i 10 . . . . 5
11850a1i 10 . . . . 5
1199adantl 445 . . . . . . 7
120119, 13syl 15 . . . . . 6
121 expcl 8823 . . . . . . 7
12226, 9, 121syl2an 456 . . . . . 6
123120, 122eqeltrd 1991 . . . . 5
124 absexp 9235 . . . . . . 7
12526, 9, 124syl2an 456 . . . . . 6
126120fveq2d 4721 . . . . . 6
12763adantl 445 . . . . . 6
128125, 126, 1273eqtr4rd 1961 . . . . 5
1291, 116, 117, 118, 123, 128climabs0 9378 . . . 4
130129biimpar 464 . . 3
131115, 130syldan 449 . 2
13221, 131pm2.61dane 2110 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 174   wa 357   wceq 1414   wcel 1416   wne 2035  cvv 2324   class class class wbr 3370  cfv 4019  (class class class)co 4979   cmpt 5140  cc 7168  cr 7169  cc0 7170  c1 7171   caddc 7173   cmul 7175   cle 7278   clt 7282   cmin 7393   cdiv 7395  cn 7396  cn0 7397  cz 7398  crp 7400  cexp 8806  cabs 9143   cli 9312
This theorem is referenced by:  explecnv 9586  geolim 9588  geo2lim 9592  mbfi1fseqlem6 13086  geomcau 18523
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 3456  ax-sep 3466  ax-nul 3475  ax-pow 3511  ax-pr 3535  ax-un 3809  ax-inf2 6217  ax-resscn 7224  ax-1cn 7225  ax-icn 7226  ax-addcl 7227  ax-addrcl 7228  ax-mulcl 7229  ax-mulrcl 7230  ax-mulcom 7231  ax-addass 7232  ax-mulass 7233  ax-distr 7234  ax-i2m1 7235  ax-1ne0 7236  ax-1rid 7237  ax-rnegex 7238  ax-rrecex 7239  ax-cnre 7240  ax-pre-lttri 7241  ax-pre-lttrn 7242  ax-pre-ltadd 7243  ax-pre-mulgt0 7244  ax-pre-sup 7245
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 2326  df-sbc 2493  df-csb 2575  df-dif 2637  df-un 2639  df-in 2641  df-ss 2645  df-pss 2647  df-nul 2903  df-if 3009  df-pw 3068  df-sn 3085  df-pr 3086  df-tp 3087  df-op 3088  df-uni 3224  df-iun 3297  df-br 3371  df-opab 3425  df-tr 3440  df-eprel 3620  df-id 3623  df-po 3628  df-so 3642  df-fr 3662  df-we 3678  df-ord 3694  df-on 3695  df-lim 3696  df-suc 3697  df-om 3974  df-xp 4021  df-rel 4022  df-cnv 4023  df-co 4024  df-dm 4025  df-rn 4026  df-res 4027  df-ima 4028  df-fun 4029  df-fn 4030  df-f 4031  df-f1 4032  df-fo 4033  df-f1o 4034  df-fv 4035  df-ov 4981  df-oprab 4982  df-mpt 5142  df-mpt2 5143  df-1st 5269  df-2nd 5270  df-iota 5377  df-rdg 5468  df-er 5643  df-map 5735  df-pm 5736  df-en 5800  df-dom 5801  df-sdom 5802  df-riota 5951  df-sup 6131  df-pnf 7283  df-mnf 7284  df-xr 7285  df-ltxr 7286  df-le 7287  df-sub 7412  df-neg 7414  df-div 7638  df-n 7877  df-2 7923  df-3 7924  df-n0 8049  df-z 8094  df-uz 8214  df-q 8296  df-rp 8421  df-fl 8660  df-seq 8754  df-exp 8807  df-cj 9050  df-re 9051  df-im 9052  df-sqr 9144  df-abs 9145  df-clim 9315  df-rlim 9316
Copyright terms: Public domain