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

Theorem expcnv 10926
Description: A sequence of powers of a complex number  A with absolute value smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.) (Proof shortened by Mario Carneiro, 26-Apr-2014.)
Hypotheses
Ref Expression
expcnv.1  |-  ( ph  ->  A  e.  CC )
expcnv.2  |-  ( ph  ->  ( abs `  A
)  <  1 )
Assertion
Ref Expression
expcnv  |-  ( ph  ->  ( n  e.  NN0  |->  ( A ^ n ) )  ~~>  0 )
Distinct variable group:    A, n
Allowed substitution hint:    ph( n)

Proof of Theorem expcnv
StepHypRef Expression
1 nnuz 9347 . . 3  |-  NN  =  ( ZZ>= `  1 )
2 1z 9146 . . . 4  |-  1  e.  ZZ
32a1i 10 . . 3  |-  ( (
ph  /\  A  = 
0 )  ->  1  e.  ZZ )
4 nn0ex 9071 . . . . 5  |-  NN0  e.  _V
54mptex 5188 . . . 4  |-  ( n  e.  NN0  |->  ( A ^ n ) )  e.  _V
65a1i 10 . . 3  |-  ( (
ph  /\  A  = 
0 )  ->  (
n  e.  NN0  |->  ( A ^ n ) )  e.  _V )
7 0cn 8250 . . . 4  |-  0  e.  CC
87a1i 10 . . 3  |-  ( (
ph  /\  A  = 
0 )  ->  0  e.  CC )
9 nnnn0 9072 . . . . . 6  |-  ( k  e.  NN  ->  k  e.  NN0 )
10 oveq2 5361 . . . . . . 7  |-  ( n  =  k  ->  ( A ^ n )  =  ( A ^ k
) )
11 eqid 2061 . . . . . . 7  |-  ( n  e.  NN0  |->  ( A ^ n ) )  =  ( n  e. 
NN0  |->  ( A ^
n ) )
12 ovex 5378 . . . . . . 7  |-  ( A ^ k )  e. 
_V
1310, 11, 12fvmpt 5114 . . . . . 6  |-  ( k  e.  NN0  ->  ( ( n  e.  NN0  |->  ( A ^ n ) ) `
 k )  =  ( A ^ k
) )
149, 13syl 15 . . . . 5  |-  ( k  e.  NN  ->  (
( n  e.  NN0  |->  ( A ^ n ) ) `  k )  =  ( A ^
k ) )
15 simpr 440 . . . . . 6  |-  ( (
ph  /\  A  = 
0 )  ->  A  =  0 )
1615oveq1d 5368 . . . . 5  |-  ( (
ph  /\  A  = 
0 )  ->  ( A ^ k )  =  ( 0 ^ k
) )
1714, 16sylan9eqr 2115 . . . 4  |-  ( ( ( ph  /\  A  =  0 )  /\  k  e.  NN )  ->  ( ( n  e. 
NN0  |->  ( A ^
n ) ) `  k )  =  ( 0 ^ k ) )
18 0exp 10122 . . . . 5  |-  ( k  e.  NN  ->  (
0 ^ k )  =  0 )
1918adantl 445 . . . 4  |-  ( ( ( ph  /\  A  =  0 )  /\  k  e.  NN )  ->  ( 0 ^ k
)  =  0 )
2017, 19eqtrd 2093 . . 3  |-  ( ( ( ph  /\  A  =  0 )  /\  k  e.  NN )  ->  ( ( n  e. 
NN0  |->  ( A ^
n ) ) `  k )  =  0 )
211, 3, 6, 8, 20climconst 10675 . 2  |-  ( (
ph  /\  A  = 
0 )  ->  (
n  e.  NN0  |->  ( A ^ n ) )  ~~>  0 )
222a1i 10 . . . 4  |-  ( (
ph  /\  A  =/=  0 )  ->  1  e.  ZZ )
23 expcnv.2 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  A
)  <  1 )
2423adantr 444 . . . . . . . . . 10  |-  ( (
ph  /\  A  =/=  0 )  ->  ( abs `  A )  <  1 )
25 expcnv.1 . . . . . . . . . . . 12  |-  ( ph  ->  A  e.  CC )
26 absrpcl 10537 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  A  =/=  0 )  -> 
( abs `  A
)  e.  RR+ )
2725, 26sylan 450 . . . . . . . . . . 11  |-  ( (
ph  /\  A  =/=  0 )  ->  ( abs `  A )  e.  RR+ )
28 elrp 9438 . . . . . . . . . . . 12  |-  ( ( abs `  A )  e.  RR+  <->  ( ( abs `  A )  e.  RR  /\  0  <  ( abs `  A ) ) )
29 reclt1 8815 . . . . . . . . . . . 12  |-  ( ( ( abs `  A
)  e.  RR  /\  0  <  ( abs `  A
) )  ->  (
( abs `  A
)  <  1  <->  1  <  ( 1  /  ( abs `  A ) ) ) )
3028, 29sylbi 185 . . . . . . . . . . 11  |-  ( ( abs `  A )  e.  RR+  ->  ( ( abs `  A )  <  1  <->  1  <  ( 1  /  ( abs `  A ) ) ) )
3127, 30syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  A  =/=  0 )  ->  (
( abs `  A
)  <  1  <->  1  <  ( 1  /  ( abs `  A ) ) ) )
3224, 31mpbid 199 . . . . . . . . 9  |-  ( (
ph  /\  A  =/=  0 )  ->  1  <  ( 1  /  ( abs `  A ) ) )
33 1re 8258 . . . . . . . . . 10  |-  1  e.  RR
34 rpreccl 9458 . . . . . . . . . . . 12  |-  ( ( abs `  A )  e.  RR+  ->  ( 1  /  ( abs `  A
) )  e.  RR+ )
3527, 34syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  A  =/=  0 )  ->  (
1  /  ( abs `  A ) )  e.  RR+ )
36 rpre 9441 . . . . . . . . . . 11  |-  ( ( 1  /  ( abs `  A ) )  e.  RR+  ->  ( 1  / 
( abs `  A
) )  e.  RR )
3735, 36syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  A  =/=  0 )  ->  (
1  /  ( abs `  A ) )  e.  RR )
38 difrp 9467 . . . . . . . . . 10  |-  ( ( 1  e.  RR  /\  ( 1  /  ( abs `  A ) )  e.  RR )  -> 
( 1  <  (
1  /  ( abs `  A ) )  <->  ( (
1  /  ( abs `  A ) )  - 
1 )  e.  RR+ ) )
3933, 37, 38sylancr 635 . . . . . . . . 9  |-  ( (
ph  /\  A  =/=  0 )  ->  (
1  <  ( 1  /  ( abs `  A
) )  <->  ( (
1  /  ( abs `  A ) )  - 
1 )  e.  RR+ ) )
4032, 39mpbid 199 . . . . . . . 8  |-  ( (
ph  /\  A  =/=  0 )  ->  (
( 1  /  ( abs `  A ) )  -  1 )  e.  RR+ )
41 rpreccl 9458 . . . . . . . 8  |-  ( ( ( 1  /  ( abs `  A ) )  -  1 )  e.  RR+  ->  ( 1  / 
( ( 1  / 
( abs `  A
) )  -  1 ) )  e.  RR+ )
4240, 41syl 15 . . . . . . 7  |-  ( (
ph  /\  A  =/=  0 )  ->  (
1  /  ( ( 1  /  ( abs `  A ) )  - 
1 ) )  e.  RR+ )
43 rpre 9441 . . . . . . 7  |-  ( ( 1  /  ( ( 1  /  ( abs `  A ) )  - 
1 ) )  e.  RR+  ->  ( 1  / 
( ( 1  / 
( abs `  A
) )  -  1 ) )  e.  RR )
4442, 43syl 15 . . . . . 6  |-  ( (
ph  /\  A  =/=  0 )  ->  (
1  /  ( ( 1  /  ( abs `  A ) )  - 
1 ) )  e.  RR )
4544recnd 8239 . . . . 5  |-  ( (
ph  /\  A  =/=  0 )  ->  (
1  /  ( ( 1  /  ( abs `  A ) )  - 
1 ) )  e.  CC )
46 divcnv 10917 . . . . 5  |-  ( ( 1  /  ( ( 1  /  ( abs `  A ) )  - 
1 ) )  e.  CC  ->  ( n  e.  NN  |->  ( ( 1  /  ( ( 1  /  ( abs `  A
) )  -  1 ) )  /  n
) )  ~~>  0 )
4745, 46syl 15 . . . 4  |-  ( (
ph  /\  A  =/=  0 )  ->  (
n  e.  NN  |->  ( ( 1  /  (
( 1  /  ( abs `  A ) )  -  1 ) )  /  n ) )  ~~>  0 )
48 nnex 8878 . . . . . 6  |-  NN  e.  _V
4948mptex 5188 . . . . 5  |-  ( n  e.  NN  |->  ( ( abs `  A ) ^ n ) )  e.  _V
5049a1i 10 . . . 4  |-  ( (
ph  /\  A  =/=  0 )  ->  (
n  e.  NN  |->  ( ( abs `  A
) ^ n ) )  e.  _V )
51 oveq2 5361 . . . . . . 7  |-  ( n  =  k  ->  (
( 1  /  (
( 1  /  ( abs `  A ) )  -  1 ) )  /  n )  =  ( ( 1  / 
( ( 1  / 
( abs `  A
) )  -  1 ) )  /  k
) )
52 eqid 2061 . . . . . . 7  |-  ( n  e.  NN  |->  ( ( 1  /  ( ( 1  /  ( abs `  A ) )  - 
1 ) )  /  n ) )  =  ( n  e.  NN  |->  ( ( 1  / 
( ( 1  / 
( abs `  A
) )  -  1 ) )  /  n
) )
53 ovex 5378 . . . . . . 7  |-  ( ( 1  /  ( ( 1  /  ( abs `  A ) )  - 
1 ) )  / 
k )  e.  _V
5451, 52, 53fvmpt 5114 . . . . . 6  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( ( 1  / 
( ( 1  / 
( abs `  A
) )  -  1 ) )  /  n
) ) `  k
)  =  ( ( 1  /  ( ( 1  /  ( abs `  A ) )  - 
1 ) )  / 
k ) )
5554adantl 445 . . . . 5  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( ( 1  / 
( ( 1  / 
( abs `  A
) )  -  1 ) )  /  n
) ) `  k
)  =  ( ( 1  /  ( ( 1  /  ( abs `  A ) )  - 
1 ) )  / 
k ) )
56 nndivre 8904 . . . . . 6  |-  ( ( ( 1  /  (
( 1  /  ( abs `  A ) )  -  1 ) )  e.  RR  /\  k  e.  NN )  ->  (
( 1  /  (
( 1  /  ( abs `  A ) )  -  1 ) )  /  k )  e.  RR )
5744, 56sylan 450 . . . . 5  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( 1  /  (
( 1  /  ( abs `  A ) )  -  1 ) )  /  k )  e.  RR )
5855, 57eqeltrd 2135 . . . 4  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( ( 1  / 
( ( 1  / 
( abs `  A
) )  -  1 ) )  /  n
) ) `  k
)  e.  RR )
59 oveq2 5361 . . . . . . . 8  |-  ( n  =  k  ->  (
( abs `  A
) ^ n )  =  ( ( abs `  A ) ^ k
) )
60 eqid 2061 . . . . . . . 8  |-  ( n  e.  NN  |->  ( ( abs `  A ) ^ n ) )  =  ( n  e.  NN  |->  ( ( abs `  A ) ^ n
) )
61 ovex 5378 . . . . . . . 8  |-  ( ( abs `  A ) ^ k )  e. 
_V
6259, 60, 61fvmpt 5114 . . . . . . 7  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( ( abs `  A
) ^ n ) ) `  k )  =  ( ( abs `  A ) ^ k
) )
6362adantl 445 . . . . . 6  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( ( abs `  A
) ^ n ) ) `  k )  =  ( ( abs `  A ) ^ k
) )
64 nnz 9138 . . . . . . 7  |-  ( k  e.  NN  ->  k  e.  ZZ )
65 rpexpcl 10107 . . . . . . 7  |-  ( ( ( abs `  A
)  e.  RR+  /\  k  e.  ZZ )  ->  (
( abs `  A
) ^ k )  e.  RR+ )
6627, 64, 65syl2an 456 . . . . . 6  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( abs `  A
) ^ k )  e.  RR+ )
6763, 66eqeltrd 2135 . . . . 5  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( ( abs `  A
) ^ n ) ) `  k )  e.  RR+ )
68 rpre 9441 . . . . 5  |-  ( ( ( n  e.  NN  |->  ( ( abs `  A
) ^ n ) ) `  k )  e.  RR+  ->  ( ( n  e.  NN  |->  ( ( abs `  A
) ^ n ) ) `  k )  e.  RR )
6967, 68syl 15 . . . 4  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( ( abs `  A
) ^ n ) ) `  k )  e.  RR )
70 nnrp 9444 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  k  e.  RR+ )
71 rpmulcl 9456 . . . . . . . . . . 11  |-  ( ( ( ( 1  / 
( abs `  A
) )  -  1 )  e.  RR+  /\  k  e.  RR+ )  ->  (
( ( 1  / 
( abs `  A
) )  -  1 )  x.  k )  e.  RR+ )
7240, 70, 71syl2an 456 . . . . . . . . . 10  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( ( 1  / 
( abs `  A
) )  -  1 )  x.  k )  e.  RR+ )
73 rpre 9441 . . . . . . . . . 10  |-  ( ( ( ( 1  / 
( abs `  A
) )  -  1 )  x.  k )  e.  RR+  ->  ( ( ( 1  /  ( abs `  A ) )  -  1 )  x.  k )  e.  RR )
7472, 73syl 15 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( ( 1  / 
( abs `  A
) )  -  1 )  x.  k )  e.  RR )
75 peano2re 8360 . . . . . . . . . 10  |-  ( ( ( ( 1  / 
( abs `  A
) )  -  1 )  x.  k )  e.  RR  ->  (
( ( ( 1  /  ( abs `  A
) )  -  1 )  x.  k )  +  1 )  e.  RR )
7674, 75syl 15 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( ( ( 1  /  ( abs `  A
) )  -  1 )  x.  k )  +  1 )  e.  RR )
77 rpexpcl 10107 . . . . . . . . . . 11  |-  ( ( ( 1  /  ( abs `  A ) )  e.  RR+  /\  k  e.  ZZ )  ->  (
( 1  /  ( abs `  A ) ) ^ k )  e.  RR+ )
7835, 64, 77syl2an 456 . . . . . . . . . 10  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( 1  /  ( abs `  A ) ) ^ k )  e.  RR+ )
79 rpre 9441 . . . . . . . . . 10  |-  ( ( ( 1  /  ( abs `  A ) ) ^ k )  e.  RR+  ->  ( ( 1  /  ( abs `  A
) ) ^ k
)  e.  RR )
8078, 79syl 15 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( 1  /  ( abs `  A ) ) ^ k )  e.  RR )
81 lep1 8736 . . . . . . . . . 10  |-  ( ( ( ( 1  / 
( abs `  A
) )  -  1 )  x.  k )  e.  RR  ->  (
( ( 1  / 
( abs `  A
) )  -  1 )  x.  k )  <_  ( ( ( ( 1  /  ( abs `  A ) )  -  1 )  x.  k )  +  1 ) )
8274, 81syl 15 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( ( 1  / 
( abs `  A
) )  -  1 )  x.  k )  <_  ( ( ( ( 1  /  ( abs `  A ) )  -  1 )  x.  k )  +  1 ) )
8337adantr 444 . . . . . . . . . 10  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
1  /  ( abs `  A ) )  e.  RR )
849adantl 445 . . . . . . . . . 10  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  k  e.  NN0 )
85 rpge0 9447 . . . . . . . . . . . 12  |-  ( ( 1  /  ( abs `  A ) )  e.  RR+  ->  0  <_  (
1  /  ( abs `  A ) ) )
8635, 85syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  A  =/=  0 )  ->  0  <_  ( 1  /  ( abs `  A ) ) )
8786adantr 444 . . . . . . . . . 10  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  0  <_  ( 1  /  ( abs `  A ) ) )
88 bernneq2 10210 . . . . . . . . . 10  |-  ( ( ( 1  /  ( abs `  A ) )  e.  RR  /\  k  e.  NN0  /\  0  <_ 
( 1  /  ( abs `  A ) ) )  ->  ( (
( ( 1  / 
( abs `  A
) )  -  1 )  x.  k )  +  1 )  <_ 
( ( 1  / 
( abs `  A
) ) ^ k
) )
8983, 84, 87, 88syl3anc 1137 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( ( ( 1  /  ( abs `  A
) )  -  1 )  x.  k )  +  1 )  <_ 
( ( 1  / 
( abs `  A
) ) ^ k
) )
9074, 76, 80, 82, 89letrd 8307 . . . . . . . 8  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( ( 1  / 
( abs `  A
) )  -  1 )  x.  k )  <_  ( ( 1  /  ( abs `  A
) ) ^ k
) )
91 rpcnne0 9452 . . . . . . . . . 10  |-  ( ( abs `  A )  e.  RR+  ->  ( ( abs `  A )  e.  CC  /\  ( abs `  A )  =/=  0 ) )
9227, 91syl 15 . . . . . . . . 9  |-  ( (
ph  /\  A  =/=  0 )  ->  (
( abs `  A
)  e.  CC  /\  ( abs `  A )  =/=  0 ) )
93 exprec 10128 . . . . . . . . . 10  |-  ( ( ( abs `  A
)  e.  CC  /\  ( abs `  A )  =/=  0  /\  k  e.  ZZ )  ->  (
( 1  /  ( abs `  A ) ) ^ k )  =  ( 1  /  (
( abs `  A
) ^ k ) ) )
94933expa 1107 . . . . . . . . 9  |-  ( ( ( ( abs `  A
)  e.  CC  /\  ( abs `  A )  =/=  0 )  /\  k  e.  ZZ )  ->  ( ( 1  / 
( abs `  A
) ) ^ k
)  =  ( 1  /  ( ( abs `  A ) ^ k
) ) )
9592, 64, 94syl2an 456 . . . . . . . 8  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( 1  /  ( abs `  A ) ) ^ k )  =  ( 1  /  (
( abs `  A
) ^ k ) ) )
9690, 95breqtrd 3606 . . . . . . 7  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( ( 1  / 
( abs `  A
) )  -  1 )  x.  k )  <_  ( 1  / 
( ( abs `  A
) ^ k ) ) )
97 elrp 9438 . . . . . . . . 9  |-  ( ( ( ( 1  / 
( abs `  A
) )  -  1 )  x.  k )  e.  RR+  <->  ( ( ( ( 1  /  ( abs `  A ) )  -  1 )  x.  k )  e.  RR  /\  0  <  ( ( ( 1  /  ( abs `  A ) )  -  1 )  x.  k ) ) )
98 elrp 9438 . . . . . . . . 9  |-  ( ( ( abs `  A
) ^ k )  e.  RR+  <->  ( ( ( abs `  A ) ^ k )  e.  RR  /\  0  < 
( ( abs `  A
) ^ k ) ) )
99 lerec2 8806 . . . . . . . . 9  |-  ( ( ( ( ( ( 1  /  ( abs `  A ) )  - 
1 )  x.  k
)  e.  RR  /\  0  <  ( ( ( 1  /  ( abs `  A ) )  - 
1 )  x.  k
) )  /\  (
( ( abs `  A
) ^ k )  e.  RR  /\  0  <  ( ( abs `  A
) ^ k ) ) )  ->  (
( ( ( 1  /  ( abs `  A
) )  -  1 )  x.  k )  <_  ( 1  / 
( ( abs `  A
) ^ k ) )  <->  ( ( abs `  A ) ^ k
)  <_  ( 1  /  ( ( ( 1  /  ( abs `  A ) )  - 
1 )  x.  k
) ) ) )
10097, 98, 99syl2anb 458 . . . . . . . 8  |-  ( ( ( ( ( 1  /  ( abs `  A
) )  -  1 )  x.  k )  e.  RR+  /\  (
( abs `  A
) ^ k )  e.  RR+ )  ->  (
( ( ( 1  /  ( abs `  A
) )  -  1 )  x.  k )  <_  ( 1  / 
( ( abs `  A
) ^ k ) )  <->  ( ( abs `  A ) ^ k
)  <_  ( 1  /  ( ( ( 1  /  ( abs `  A ) )  - 
1 )  x.  k
) ) ) )
10172, 66, 100syl2anc 633 . . . . . . 7  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( ( ( 1  /  ( abs `  A
) )  -  1 )  x.  k )  <_  ( 1  / 
( ( abs `  A
) ^ k ) )  <->  ( ( abs `  A ) ^ k
)  <_  ( 1  /  ( ( ( 1  /  ( abs `  A ) )  - 
1 )  x.  k
) ) ) )
10296, 101mpbid 199 . . . . . 6  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( abs `  A
) ^ k )  <_  ( 1  / 
( ( ( 1  /  ( abs `  A
) )  -  1 )  x.  k ) ) )
103 rpcnne0 9452 . . . . . . . 8  |-  ( ( ( 1  /  ( abs `  A ) )  -  1 )  e.  RR+  ->  ( ( ( 1  /  ( abs `  A ) )  - 
1 )  e.  CC  /\  ( ( 1  / 
( abs `  A
) )  -  1 )  =/=  0 ) )
10440, 103syl 15 . . . . . . 7  |-  ( (
ph  /\  A  =/=  0 )  ->  (
( ( 1  / 
( abs `  A
) )  -  1 )  e.  CC  /\  ( ( 1  / 
( abs `  A
) )  -  1 )  =/=  0 ) )
105 nncn 8880 . . . . . . . 8  |-  ( k  e.  NN  ->  k  e.  CC )
106 nnne0 8901 . . . . . . . 8  |-  ( k  e.  NN  ->  k  =/=  0 )
107105, 106jca 511 . . . . . . 7  |-  ( k  e.  NN  ->  (
k  e.  CC  /\  k  =/=  0 ) )
108 recdiv2 8717 . . . . . . 7  |-  ( ( ( ( ( 1  /  ( abs `  A
) )  -  1 )  e.  CC  /\  ( ( 1  / 
( abs `  A
) )  -  1 )  =/=  0 )  /\  ( k  e.  CC  /\  k  =/=  0 ) )  -> 
( ( 1  / 
( ( 1  / 
( abs `  A
) )  -  1 ) )  /  k
)  =  ( 1  /  ( ( ( 1  /  ( abs `  A ) )  - 
1 )  x.  k
) ) )
109104, 107, 108syl2an 456 . . . . . 6  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( 1  /  (
( 1  /  ( abs `  A ) )  -  1 ) )  /  k )  =  ( 1  /  (
( ( 1  / 
( abs `  A
) )  -  1 )  x.  k ) ) )
110102, 109breqtrrd 3608 . . . . 5  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( abs `  A
) ^ k )  <_  ( ( 1  /  ( ( 1  /  ( abs `  A
) )  -  1 ) )  /  k
) )
111110, 63, 553brtr4d 3612 . . . 4  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( ( abs `  A
) ^ n ) ) `  k )  <_  ( ( n  e.  NN  |->  ( ( 1  /  ( ( 1  /  ( abs `  A ) )  - 
1 ) )  /  n ) ) `  k ) )
112 rpge0 9447 . . . . 5  |-  ( ( ( n  e.  NN  |->  ( ( abs `  A
) ^ n ) ) `  k )  e.  RR+  ->  0  <_ 
( ( n  e.  NN  |->  ( ( abs `  A ) ^ n
) ) `  k
) )
11367, 112syl 15 . . . 4  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  0  <_  ( ( n  e.  NN  |->  ( ( abs `  A ) ^ n
) ) `  k
) )
1141, 22, 47, 50, 58, 69, 111, 113climsqz2 10729 . . 3  |-  ( (
ph  /\  A  =/=  0 )  ->  (
n  e.  NN  |->  ( ( abs `  A
) ^ n ) )  ~~>  0 )
1152a1i 10 . . . . 5  |-  ( ph  ->  1  e.  ZZ )
1165a1i 10 . . . . 5  |-  ( ph  ->  ( n  e.  NN0  |->  ( A ^ n ) )  e.  _V )
11749a1i 10 . . . . 5  |-  ( ph  ->  ( n  e.  NN  |->  ( ( abs `  A
) ^ n ) )  e.  _V )
1189adantl 445 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  k  e. 
NN0 )
119118, 13syl 15 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( n  e.  NN0  |->  ( A ^ n ) ) `
 k )  =  ( A ^ k
) )
120 expcl 10106 . . . . . . 7  |-  ( ( A  e.  CC  /\  k  e.  NN0 )  -> 
( A ^ k
)  e.  CC )
12125, 9, 120syl2an 456 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( A ^ k )  e.  CC )
122119, 121eqeltrd 2135 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( n  e.  NN0  |->  ( A ^ n ) ) `
 k )  e.  CC )
123 absexp 10552 . . . . . . 7  |-  ( ( A  e.  CC  /\  k  e.  NN0 )  -> 
( abs `  ( A ^ k ) )  =  ( ( abs `  A ) ^ k
) )
12425, 9, 123syl2an 456 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( abs `  ( A ^ k
) )  =  ( ( abs `  A
) ^ k ) )
125119fveq2d 5042 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( abs `  ( ( n  e. 
NN0  |->  ( A ^
n ) ) `  k ) )  =  ( abs `  ( A ^ k ) ) )
12662adantl 445 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( n  e.  NN  |->  ( ( abs `  A
) ^ n ) ) `  k )  =  ( ( abs `  A ) ^ k
) )
127124, 125, 1263eqtr4rd 2104 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( n  e.  NN  |->  ( ( abs `  A
) ^ n ) ) `  k )  =  ( abs `  (
( n  e.  NN0  |->  ( A ^ n ) ) `  k ) ) )
1281, 115, 116, 117, 122, 127climabs0 10704 . . . 4  |-  ( ph  ->  ( ( n  e. 
NN0  |->  ( A ^
n ) )  ~~>  0  <->  (
n  e.  NN  |->  ( ( abs `  A
) ^ n ) )  ~~>  0 ) )
129128biimpar 464 . . 3  |-  ( (
ph  /\  ( n  e.  NN  |->  ( ( abs `  A ) ^ n
) )  ~~>  0 )  ->  ( n  e. 
NN0  |->  ( A ^
n ) )  ~~>  0 )
130114, 129syldan 449 . 2  |-  ( (
ph  /\  A  =/=  0 )  ->  (
n  e.  NN0  |->  ( A ^ n ) )  ~~>  0 )
13121, 130pm2.61dane 2254 1  |-  ( ph  ->  ( n  e.  NN0  |->  ( A ^ n ) )  ~~>  0 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 174    /\ wa 356    = wceq 1517    e. wcel 1519    =/= wne 2179   _Vcvv 2472   class class class wbr 3582    e. cmpt 3636   ` cfv 4264  (class class class)co 5353   CCcc 8145   RRcr 8146   0cc0 8147   1c1 8148    + caddc 8150    x. cmul 8152    <_ cle 8260    < clt 8264    - cmin 8383    / cdiv 8385   NNcn 8386   NN0cn0 8387   ZZcz 8388   RR+crp 8390   ^cexp 10089   abscabs 10460    ~~> cli 10638
This theorem is referenced by:  explecnv  10927  geolim  10929  geo2lim  10933  iscmet3lem3  16523  mbfi1fseqlem6  16882  geomcau  23020
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1439  ax-6 1440  ax-7 1441  ax-gen 1442  ax-8 1521  ax-11 1522  ax-13 1523  ax-14 1524  ax-17 1526  ax-12o 1559  ax-10 1573  ax-9 1579  ax-4 1586  ax-16 1772  ax-ext 2043  ax-rep 3687  ax-sep 3697  ax-nul 3705  ax-pow 3741  ax-pr 3765  ax-un 4057  ax-cnex 8202  ax-resscn 8203  ax-1cn 8204  ax-icn 8205  ax-addcl 8206  ax-addrcl 8207  ax-mulcl 8208  ax-mulrcl 8209  ax-mulcom 8210  ax-addass 8211  ax-mulass 8212  ax-distr 8213  ax-i2m1 8214  ax-1ne0 8215  ax-1rid 8216  ax-rnegex 8217  ax-rrecex 8218  ax-cnre 8219  ax-pre-lttri 8220  ax-pre-lttrn 8221  ax-pre-ltadd 8222  ax-pre-mulgt0 8223  ax-pre-sup 8224
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3or 894  df-3an 895  df-tru 1256  df-ex 1444  df-sb 1733  df-eu 1955  df-mo 1956  df-clab 2049  df-cleq 2054  df-clel 2057  df-ne 2181  df-nel 2182  df-ral 2275  df-rex 2276  df-reu 2277  df-rab 2278  df-v 2474  df-sbc 2648  df-csb 2730  df-dif 2793  df-un 2795  df-in 2797  df-ss 2801  df-pss 2803  df-nul 3070  df-if 3178  df-pw 3239  df-sn 3257  df-pr 3258  df-tp 3259  df-op 3260  df-uni 3421  df-iun 3498  df-br 3583  df-opab 3637  df-mpt 3638  df-tr 3670  df-eprel 3852  df-id 3856  df-po 3861  df-so 3862  df-fr 3899  df-we 3901  df-ord 3942  df-on 3943  df-lim 3944  df-suc 3945  df-om 4220  df-xp 4266  df-rel 4267  df-cnv 4268  df-co 4269  df-dm 4270  df-rn 4271  df-res 4272  df-ima 4273  df-fun 4274  df-fn 4275  df-f 4276  df-f1 4277  df-fo 4278  df-f1o 4279  df-fv 4280  df-ov 5356  df-oprab 5357  df-mpt2 5358  df-2nd 5608  df-iota 5762  df-recs 5835  df-rdg 5870  df-er 6107  df-pm 6212  df-en 6294  df-dom 6295  df-sdom 6296  df-riota 6460  df-sup 6666  df-pnf 8265  df-mnf 8266  df-xr 8267  df-ltxr 8268  df-le 8269  df-sub 8402  df-neg 8403  df-div 8631  df-n 8873  df-2 8920  df-3 8921  df-n0 9066  df-z 9118  df-uz 9315  df-rp 9437  df-fl 9931  df-seq 10035  df-exp 10090  df-cj 10363  df-re 10364  df-im 10365  df-sqr 10461  df-abs 10462  df-clim 10641  df-rlim 10642
Copyright terms: Public domain