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

Theorem expcnv 10479
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 9094 . . 3
2 1z 8895 . . . 4
32a1i 10 . . 3
4 nn0ex 8822 . . . . 5
54mptex 5402 . . . 4
65a1i 10 . . 3
7 0cn 8007 . . . 4
87a1i 10 . . 3
9 nnnn0 8823 . . . . . 6
10 oveq2 5212 . . . . . . 7
11 eqid 2030 . . . . . . 7
12 ovex 5228 . . . . . . 7
1310, 11, 12fvmpt 5426 . . . . . 6
149, 13syl 15 . . . . 5
15 simpr 440 . . . . . 6
1615oveq1d 5218 . . . . 5
1714, 16sylan9eqr 2084 . . . 4
18 0exp 9699 . . . . 5
1918adantl 445 . . . 4
2017, 19eqtrd 2062 . . 3
211, 3, 6, 8, 20climconst 10230 . 2
222a1i 10 . . . 4
23 expcnv.2 . . . . . . . . . . 11
2423adantr 444 . . . . . . . . . 10
25 expcnv.1 . . . . . . . . . . . 12
26 absrpcl 10097 . . . . . . . . . . . 12
2725, 26sylan 450 . . . . . . . . . . 11
28 elrp 9278 . . . . . . . . . . . 12
29 reclt1 8567 . . . . . . . . . . . 12
3028, 29sylbi 185 . . . . . . . . . . 11
3127, 30syl 15 . . . . . . . . . 10
3224, 31mpbid 199 . . . . . . . . 9
33 1re 8015 . . . . . . . . . 10
34 rpreccl 9297 . . . . . . . . . . . 12
3527, 34syl 15 . . . . . . . . . . 11
36 rpre 9281 . . . . . . . . . . 11
3735, 36syl 15 . . . . . . . . . 10
38 difrp 9305 . . . . . . . . . 10
3933, 37, 38sylancr 639 . . . . . . . . 9
4032, 39mpbid 199 . . . . . . . 8
41 rpreccl 9297 . . . . . . . 8
4240, 41syl 15 . . . . . . 7
43 rpre 9281 . . . . . . 7
4442, 43syl 15 . . . . . 6
4544recnd 7996 . . . . 5
46 divcnv 10470 . . . . 5
4745, 46syl 15 . . . 4
48 nnex 8626 . . . . . 6
4948mptex 5402 . . . . 5
5049a1i 10 . . . 4
51 oveq2 5212 . . . . . . 7
52 eqid 2030 . . . . . . 7
53 ovex 5228 . . . . . . 7
5451, 52, 53fvmpt 5426 . . . . . 6
5554adantl 445 . . . . 5
56 nndivre 8655 . . . . . 6
5744, 56sylan 450 . . . . 5
5855, 57eqeltrd 2103 . . . 4
59 oveq2 5212 . . . . . . . 8
60 eqid 2030 . . . . . . . 8
61 ovex 5228 . . . . . . . 8
6259, 60, 61fvmpt 5426 . . . . . . 7
6362adantl 445 . . . . . 6
64 nnz 8887 . . . . . . 7
65 rpexpcl 9684 . . . . . . 7
6627, 64, 65syl2an 456 . . . . . 6
6763, 66eqeltrd 2103 . . . . 5
68 rpre 9281 . . . . 5
6967, 68syl 15 . . . 4
70 nnrp 9283 . . . . . . . . . . 11
71 rpmulcl 9295 . . . . . . . . . . 11
7240, 70, 71syl2an 456 . . . . . . . . . 10
73 rpre 9281 . . . . . . . . . 10
7472, 73syl 15 . . . . . . . . 9
75 peano2re 8115 . . . . . . . . . 10
7674, 75syl 15 . . . . . . . . 9
77 rpexpcl 9684 . . . . . . . . . . 11
7835, 64, 77syl2an 456 . . . . . . . . . 10
79 rpre 9281 . . . . . . . . . 10
8078, 79syl 15 . . . . . . . . 9
81 lep1 8489 . . . . . . . . . 10
8274, 81syl 15 . . . . . . . . 9
8337adantr 444 . . . . . . . . . 10
849adantl 445 . . . . . . . . . 10
85 rpge0 9286 . . . . . . . . . . . 12
8635, 85syl 15 . . . . . . . . . . 11
8786adantr 444 . . . . . . . . . 10
88 bernneq2 9783 . . . . . . . . . 10
8983, 84, 87, 88syl3anc 1142 . . . . . . . . 9
9074, 76, 80, 82, 89letrd 8066 . . . . . . . 8
91 rpcnne0 9291 . . . . . . . . . 10
9227, 91syl 15 . . . . . . . . 9
93 exprec 9705 . . . . . . . . . 10
94933expa 1112 . . . . . . . . 9
9592, 64, 94syl2an 456 . . . . . . . 8
9690, 95breqtrd 3555 . . . . . . 7
97 elrp 9278 . . . . . . . . 9
98 elrp 9278 . . . . . . . . 9
99 lerec2 8558 . . . . . . . . 9
10097, 98, 99syl2anb 458 . . . . . . . 8
10172, 66, 100syl2anc 637 . . . . . . 7
10296, 101mpbid 199 . . . . . 6
103 rpcnne0 9291 . . . . . . . 8
10440, 103syl 15 . . . . . . 7
105 nncn 8631 . . . . . . . 8
106 nnne0 8652 . . . . . . . 8
107105, 106jca 513 . . . . . . 7
108 recdiv2 8470 . . . . . . 7
109104, 107, 108syl2an 456 . . . . . 6
110102, 109breqtrrd 3557 . . . . 5
111110, 63, 553brtr4d 3561 . . . 4
112 rpge0 9286 . . . . 5
11367, 112syl 15 . . . 4
1141, 22, 47, 50, 58, 69, 111, 113climsqz2 10284 . . 3
1152a1i 10 . . . . 5
1165a1i 10 . . . . 5
11749a1i 10 . . . . 5
1189adantl 445 . . . . . . 7
119118, 13syl 15 . . . . . 6
120 expcl 9683 . . . . . . 7
12125, 9, 120syl2an 456 . . . . . 6
122119, 121eqeltrd 2103 . . . . 5
123 absexp 10112 . . . . . . 7
12425, 9, 123syl2an 456 . . . . . 6
125119fveq2d 4914 . . . . . 6
12662adantl 445 . . . . . 6
127124, 125, 1263eqtr4rd 2073 . . . . 5
1281, 115, 116, 117, 122, 127climabs0 10259 . . . 4
129128biimpar 464 . . 3
130114, 129syldan 449 . 2
13121, 130pm2.61dane 2222 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 174   wa 357   wceq 1526   wcel 1528   wne 2147  cvv 2440   class class class wbr 3531  cfv 4184  (class class class)co 5206   cmpt 5369  cc 7906  cr 7907  cc0 7908  c1 7909   caddc 7911   cmul 7913   cle 8017   clt 8021   cmin 8138   cdiv 8140  cn 8141  cn0 8142  cz 8143  crp 8145  cexp 9666  cabs 10020   cli 10193
This theorem is referenced by:  explecnv 10480  geolim 10482  geo2lim 10486  mbfi1fseqlem6 14638  geomcau 20872
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-7 1445  ax-gen 1446  ax-8 1530  ax-10 1531  ax-11 1532  ax-12 1533  ax-13 1534  ax-14 1535  ax-17 1542  ax-9 1557  ax-4 1563  ax-16 1741  ax-ext 2012  ax-rep 3616  ax-sep 3626  ax-nul 3635  ax-pow 3671  ax-pr 3695  ax-un 3973  ax-inf2 6607  ax-resscn 7962  ax-1cn 7963  ax-icn 7964  ax-addcl 7965  ax-addrcl 7966  ax-mulcl 7967  ax-mulrcl 7968  ax-mulcom 7969  ax-addass 7970  ax-mulass 7971  ax-distr 7972  ax-i2m1 7973  ax-1ne0 7974  ax-1rid 7975  ax-rnegex 7976  ax-rrecex 7977  ax-cnre 7978  ax-pre-lttri 7979  ax-pre-lttrn 7980  ax-pre-ltadd 7981  ax-pre-mulgt0 7982  ax-pre-sup 7983
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1261  df-ex 1448  df-sb 1703  df-eu 1930  df-mo 1931  df-clab 2018  df-cleq 2023  df-clel 2026  df-ne 2149  df-nel 2150  df-ral 2243  df-rex 2244  df-reu 2245  df-rab 2246  df-v 2442  df-sbc 2609  df-csb 2691  df-dif 2753  df-un 2755  df-in 2757  df-ss 2761  df-pss 2763  df-nul 3026  df-if 3135  df-pw 3196  df-sn 3214  df-pr 3215  df-tp 3216  df-op 3217  df-uni 3375  df-iun 3451  df-br 3532  df-opab 3585  df-tr 3600  df-eprel 3783  df-id 3787  df-po 3792  df-so 3806  df-fr 3826  df-we 3842  df-ord 3858  df-on 3859  df-lim 3860  df-suc 3861  df-om 4139  df-xp 4186  df-rel 4187  df-cnv 4188  df-co 4189  df-dm 4190  df-rn 4191  df-res 4192  df-ima 4193  df-fun 4194  df-fn 4195  df-f 4196  df-f1 4197  df-fo 4198  df-f1o 4199  df-fv 4200  df-ov 5208  df-oprab 5209  df-mpt 5371  df-mpt2 5372  df-1st 5521  df-2nd 5522  df-iota 5647  df-recs 5722  df-rdg 5750  df-er 5952  df-map 6044  df-pm 6045  df-en 6121  df-dom 6122  df-sdom 6123  df-riota 6281  df-sup 6474  df-pnf 8022  df-mnf 8023  df-xr 8024  df-ltxr 8025  df-le 8026  df-sub 8157  df-neg 8159  df-div 8385  df-n 8625  df-2 8671  df-3 8672  df-n0 8817  df-z 8868  df-uz 9062  df-q 9148  df-rp 9277  df-fl 9512  df-seq 9612  df-exp 9667  df-cj 9923  df-re 9924  df-im 9925  df-sqr 10021  df-abs 10022  df-clim 10196  df-rlim 10197
Copyright terms: Public domain