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

Theorem expcnv 9669
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 8303 . . 3
2 1z 8177 . . . 4
32a1i 10 . . 3
4 nn0ex 8110 . . . . 5
54mptex 5196 . . . 4
65a1i 10 . . 3
7 0cn 7310 . . . 4
87a1i 10 . . 3
9 nnnn0 8111 . . . . . 6
10 oveq2 5008 . . . . . . 7
11 eqid 1918 . . . . . . 7
12 ovex 5024 . . . . . . 7
1310, 11, 12fvmpt 5219 . . . . . 6
149, 13syl 15 . . . . 5
15 simpr 440 . . . . . 6
1615oveq1d 5014 . . . . 5
1714, 16sylan9eqr 1972 . . . 4
18 0exp 8902 . . . . 5
1918adantl 445 . . . 4
2017, 19eqtrd 1950 . . 3
211, 3, 6, 8, 20climconst 9424 . 2
222a1i 10 . . . 4
237a1i 10 . . . 4
24 expcnv.2 . . . . . . . . . . 11
2524adantr 444 . . . . . . . . . 10
26 expcnv.1 . . . . . . . . . . . 12
27 absrpcl 9292 . . . . . . . . . . . 12
2826, 27sylan 450 . . . . . . . . . . 11
29 elrp 8482 . . . . . . . . . . . 12
30 reclt1 7863 . . . . . . . . . . . 12
3129, 30sylbi 185 . . . . . . . . . . 11
3228, 31syl 15 . . . . . . . . . 10
3325, 32mpbid 199 . . . . . . . . 9
34 1re 7318 . . . . . . . . . 10
35 rpreccl 8501 . . . . . . . . . . . 12
3628, 35syl 15 . . . . . . . . . . 11
37 rpre 8485 . . . . . . . . . . 11
3836, 37syl 15 . . . . . . . . . 10
39 difrp 8509 . . . . . . . . . 10
4034, 38, 39sylancr 639 . . . . . . . . 9
4133, 40mpbid 199 . . . . . . . 8
42 rpreccl 8501 . . . . . . . 8
4341, 42syl 15 . . . . . . 7
44 rpre 8485 . . . . . . 7
4543, 44syl 15 . . . . . 6
4645recnd 7300 . . . . 5
47 divcnv 9663 . . . . 5
4846, 47syl 15 . . . 4
49 nnex 7922 . . . . . 6
5049mptex 5196 . . . . 5
5150a1i 10 . . . 4
52 oveq2 5008 . . . . . . 7
53 eqid 1918 . . . . . . 7
54 ovex 5024 . . . . . . 7
5552, 53, 54fvmpt 5219 . . . . . 6
5655adantl 445 . . . . 5
57 nndivre 7951 . . . . . 6
5845, 57sylan 450 . . . . 5
5956, 58eqeltrd 1991 . . . 4
60 oveq2 5008 . . . . . . . 8
61 eqid 1918 . . . . . . . 8
62 ovex 5024 . . . . . . . 8
6360, 61, 62fvmpt 5219 . . . . . . 7
6463adantl 445 . . . . . 6
65 nnz 8169 . . . . . . 7
66 rpexpcl 8890 . . . . . . 7
6728, 65, 66syl2an 456 . . . . . 6
6864, 67eqeltrd 1991 . . . . 5
69 rpre 8485 . . . . 5
7068, 69syl 15 . . . 4
71 nnrp 8487 . . . . . . . . . . 11
72 rpmulcl 8499 . . . . . . . . . . 11
7341, 71, 72syl2an 456 . . . . . . . . . 10
74 rpre 8485 . . . . . . . . . 10
7573, 74syl 15 . . . . . . . . 9
76 peano2re 7414 . . . . . . . . . 10
7775, 76syl 15 . . . . . . . . 9
78 rpexpcl 8890 . . . . . . . . . . 11
7936, 65, 78syl2an 456 . . . . . . . . . 10
80 rpre 8485 . . . . . . . . . 10
8179, 80syl 15 . . . . . . . . 9
82 lep1 7785 . . . . . . . . . 10
8375, 82syl 15 . . . . . . . . 9
8438adantr 444 . . . . . . . . . 10
859adantl 445 . . . . . . . . . 10
86 rpge0 8490 . . . . . . . . . . . 12
8736, 86syl 15 . . . . . . . . . . 11
8887adantr 444 . . . . . . . . . 10
89 bernneq2 8985 . . . . . . . . . 10
9084, 85, 88, 89syl3anc 1142 . . . . . . . . 9
9175, 77, 81, 83, 90letrd 7365 . . . . . . . 8
92 rpcnne0 8495 . . . . . . . . . 10
9328, 92syl 15 . . . . . . . . 9
94 exprec 8908 . . . . . . . . . 10
95943expa 1112 . . . . . . . . 9
9693, 65, 95syl2an 456 . . . . . . . 8
9791, 96breqtrd 3407 . . . . . . 7
98 elrp 8482 . . . . . . . . 9
99 elrp 8482 . . . . . . . . 9
100 lerec2 7854 . . . . . . . . 9
10198, 99, 100syl2anb 458 . . . . . . . 8
10273, 67, 101syl2anc 637 . . . . . . 7
10397, 102mpbid 199 . . . . . 6
104 rpcnne0 8495 . . . . . . . 8
10541, 104syl 15 . . . . . . 7
106 nncn 7927 . . . . . . . 8
107 nnne0 7948 . . . . . . . 8
108106, 107jca 513 . . . . . . 7
109 recdiv2 7767 . . . . . . 7
110105, 108, 109syl2an 456 . . . . . 6
111103, 110breqtrrd 3409 . . . . 5
112111, 64, 563brtr4d 3413 . . . 4
113 rpge0 8490 . . . . 5
11468, 113syl 15 . . . 4
1151, 22, 23, 48, 51, 59, 70, 112, 114climsqz2 9478 . . 3
1162a1i 10 . . . . 5
1175a1i 10 . . . . 5
11850a1i 10 . . . . 5
1199adantl 445 . . . . . . 7
120119, 13syl 15 . . . . . 6
121 expcl 8889 . . . . . . 7
12226, 9, 121syl2an 456 . . . . . 6
123120, 122eqeltrd 1991 . . . . 5
124 absexp 9307 . . . . . . 7
12526, 9, 124syl2an 456 . . . . . 6
126120fveq2d 4739 . . . . . 6
12763adantl 445 . . . . . 6
128125, 126, 1273eqtr4rd 1961 . . . . 5
1291, 116, 117, 118, 123, 128climabs0 9453 . . . 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 2326   class class class wbr 3383  cfv 4033  (class class class)co 5002   cmpt 5163  cc 7210  cr 7211  cc0 7212  c1 7213   caddc 7215   cmul 7217   cle 7320   clt 7324   cmin 7436   cdiv 7438  cn 7439  cn0 7440  cz 7441  crp 7443  cexp 8872  cabs 9215   cli 9387
This theorem is referenced by:  explecnv 9670  geolim 9672  geo2lim 9676  mbfi1fseqlem6 13570  geomcau 19242
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 3469  ax-sep 3479  ax-nul 3488  ax-pow 3524  ax-pr 3548  ax-un 3823  ax-inf2 6256  ax-resscn 7266  ax-1cn 7267  ax-icn 7268  ax-addcl 7269  ax-addrcl 7270  ax-mulcl 7271  ax-mulrcl 7272  ax-mulcom 7273  ax-addass 7274  ax-mulass 7275  ax-distr 7276  ax-i2m1 7277  ax-1ne0 7278  ax-1rid 7279  ax-rnegex 7280  ax-rrecex 7281  ax-cnre 7282  ax-pre-lttri 7283  ax-pre-lttrn 7284  ax-pre-ltadd 7285  ax-pre-mulgt0 7286  ax-pre-sup 7287
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 2328  df-sbc 2495  df-csb 2577  df-dif 2639  df-un 2641  df-in 2643  df-ss 2647  df-pss 2649  df-nul 2905  df-if 3012  df-pw 3072  df-sn 3089  df-pr 3090  df-tp 3091  df-op 3092  df-uni 3234  df-iun 3307  df-br 3384  df-opab 3438  df-tr 3453  df-eprel 3634  df-id 3637  df-po 3642  df-so 3656  df-fr 3676  df-we 3692  df-ord 3708  df-on 3709  df-lim 3710  df-suc 3711  df-om 3988  df-xp 4035  df-rel 4036  df-cnv 4037  df-co 4038  df-dm 4039  df-rn 4040  df-res 4041  df-ima 4042  df-fun 4043  df-fn 4044  df-f 4045  df-f1 4046  df-fo 4047  df-f1o 4048  df-fv 4049  df-ov 5004  df-oprab 5005  df-mpt 5165  df-mpt2 5166  df-1st 5296  df-2nd 5297  df-iota 5407  df-rdg 5498  df-er 5673  df-map 5765  df-pm 5766  df-en 5830  df-dom 5831  df-sdom 5832  df-riota 5987  df-sup 6170  df-pnf 7325  df-mnf 7326  df-xr 7327  df-ltxr 7328  df-le 7329  df-sub 7455  df-neg 7457  df-div 7682  df-n 7921  df-2 7967  df-3 7968  df-n0 8105  df-z 8150  df-uz 8272  df-q 8354  df-rp 8481  df-fl 8724  df-seq 8819  df-exp 8873  df-cj 9120  df-re 9121  df-im 9122  df-sqr 9216  df-abs 9217  df-clim 9390  df-rlim 9391
Copyright terms: Public domain