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

Theorem expcnv 10984
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 9358 . . 3  |-  NN  =  ( ZZ>= `  1 )
2 1z 9156 . . . 4  |-  1  e.  ZZ
32a1i 10 . . 3  |-  ( (
ph  /\  A  = 
0 )  ->  1  e.  ZZ )
4 nn0ex 9081 . . . . 5  |-  NN0  e.  _V
54mptex 5191 . . . 4  |-  ( n  e.  NN0  |->  ( A ^ n ) )  e.  _V
65a1i 10 . . 3  |-  ( (
ph  /\  A  = 
0 )  ->  (
n  e.  NN0  |->  ( A ^ n ) )  e.  _V )
7 0cn 8256 . . . 4  |-  0  e.  CC
87a1i 10 . . 3  |-  ( (
ph  /\  A  = 
0 )  ->  0  e.  CC )
9 nnnn0 9082 . . . . . 6  |-  ( k  e.  NN  ->  k  e.  NN0 )
10 oveq2 5364 . . . . . . 7  |-  ( n  =  k  ->  ( A ^ n )  =  ( A ^ k
) )
11 eqid 2062 . . . . . . 7  |-  ( n  e.  NN0  |->  ( A ^ n ) )  =  ( n  e. 
NN0  |->  ( A ^
n ) )
12 ovex 5381 . . . . . . 7  |-  ( A ^ k )  e. 
_V
1310, 11, 12fvmpt 5117 . . . . . 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 5371 . . . . 5  |-  ( (
ph  /\  A  = 
0 )  ->  ( A ^ k )  =  ( 0 ^ k
) )
1714, 16sylan9eqr 2116 . . . 4  |-  ( ( ( ph  /\  A  =  0 )  /\  k  e.  NN )  ->  ( ( n  e. 
NN0  |->  ( A ^
n ) ) `  k )  =  ( 0 ^ k ) )
18 0exp 10144 . . . . 5  |-  ( k  e.  NN  ->  (
0 ^ k )  =  0 )
1918adantl 445 . . . 4  |-  ( ( ( ph  /\  A  =  0 )  /\  k  e.  NN )  ->  ( 0 ^ k
)  =  0 )
2017, 19eqtrd 2094 . . 3  |-  ( ( ( ph  /\  A  =  0 )  /\  k  e.  NN )  ->  ( ( n  e. 
NN0  |->  ( A ^
n ) ) `  k )  =  0 )
211, 3, 6, 8, 20climconst 10709 . 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 10563 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  A  =/=  0 )  -> 
( abs `  A
)  e.  RR+ )
2725, 26sylan 450 . . . . . . . . . . 11  |-  ( (
ph  /\  A  =/=  0 )  ->  ( abs `  A )  e.  RR+ )
28 elrp 9449 . . . . . . . . . . . 12  |-  ( ( abs `  A )  e.  RR+  <->  ( ( abs `  A )  e.  RR  /\  0  <  ( abs `  A ) ) )
29 reclt1 8825 . . . . . . . . . . . 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 8264 . . . . . . . . . 10  |-  1  e.  RR
34 rpreccl 9469 . . . . . . . . . . . 12  |-  ( ( abs `  A )  e.  RR+  ->  ( 1  /  ( abs `  A
) )  e.  RR+ )
3527, 34syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  A  =/=  0 )  ->  (
1  /  ( abs `  A ) )  e.  RR+ )
36 rpre 9452 . . . . . . . . . . 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 9478 . . . . . . . . . 10  |-  ( ( 1  e.  RR  /\  ( 1  /  ( abs `  A ) )  e.  RR )  -> 
( 1  <  (
1  /  ( abs `  A ) )  <->  ( (
1  /  ( abs `  A ) )  - 
1 )  e.  RR+ ) )
3933, 37, 38sylancr 636 . . . . . . . . 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 9469 . . . . . . . 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 9452 . . . . . . 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 8245 . . . . 5  |-  ( (
ph  /\  A  =/=  0 )  ->  (
1  /  ( ( 1  /  ( abs `  A ) )  - 
1 ) )  e.  CC )
46 divcnv 10975 . . . . 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 8888 . . . . . 6  |-  NN  e.  _V
4948mptex 5191 . . . . 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 5364 . . . . . . 7  |-  ( n  =  k  ->  (
( 1  /  (
( 1  /  ( abs `  A ) )  -  1 ) )  /  n )  =  ( ( 1  / 
( ( 1  / 
( abs `  A
) )  -  1 ) )  /  k
) )
52 eqid 2062 . . . . . . 7  |-  ( n  e.  NN  |->  ( ( 1  /  ( ( 1  /  ( abs `  A ) )  - 
1 ) )  /  n ) )  =  ( n  e.  NN  |->  ( ( 1  / 
( ( 1  / 
( abs `  A
) )  -  1 ) )  /  n
) )
53 ovex 5381 . . . . . . 7  |-  ( ( 1  /  ( ( 1  /  ( abs `  A ) )  - 
1 ) )  / 
k )  e.  _V
5451, 52, 53fvmpt 5117 . . . . . 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 8914 . . . . . 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 2136 . . . 4  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( ( 1  / 
( ( 1  / 
( abs `  A
) )  -  1 ) )  /  n
) ) `  k
)  e.  RR )
59 oveq2 5364 . . . . . . . 8  |-  ( n  =  k  ->  (
( abs `  A
) ^ n )  =  ( ( abs `  A ) ^ k
) )
60 eqid 2062 . . . . . . . 8  |-  ( n  e.  NN  |->  ( ( abs `  A ) ^ n ) )  =  ( n  e.  NN  |->  ( ( abs `  A ) ^ n
) )
61 ovex 5381 . . . . . . . 8  |-  ( ( abs `  A ) ^ k )  e. 
_V
6259, 60, 61fvmpt 5117 . . . . . . 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 9148 . . . . . . 7  |-  ( k  e.  NN  ->  k  e.  ZZ )
65 rpexpcl 10129 . . . . . . 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 2136 . . . . 5  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( ( abs `  A
) ^ n ) ) `  k )  e.  RR+ )
68 rpre 9452 . . . . 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 9455 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  k  e.  RR+ )
71 rpmulcl 9467 . . . . . . . . . . 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 9452 . . . . . . . . . 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 8366 . . . . . . . . . 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 10129 . . . . . . . . . . 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 9452 . . . . . . . . . 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 8746 . . . . . . . . . 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 9458 . . . . . . . . . . . 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 10234 . . . . . . . . . 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 1138 . . . . . . . . 9  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( ( ( 1  /  ( abs `  A
) )  -  1 )  x.  k )  +  1 )  <_ 
( ( 1  / 
( abs `  A
) ) ^ k
) )
9074, 76, 80, 82, 89letrd 8313 . . . . . . . 8  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( ( 1  / 
( abs `  A
) )  -  1 )  x.  k )  <_  ( ( 1  /  ( abs `  A
) ) ^ k
) )
91 rpcnne0 9463 . . . . . . . . . 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 10150 . . . . . . . . . 10  |-  ( ( ( abs `  A
)  e.  CC  /\  ( abs `  A )  =/=  0  /\  k  e.  ZZ )  ->  (
( 1  /  ( abs `  A ) ) ^ k )  =  ( 1  /  (
( abs `  A
) ^ k ) ) )
94933expa 1108 . . . . . . . . 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 3608 . . . . . . 7  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( ( 1  / 
( abs `  A
) )  -  1 )  x.  k )  <_  ( 1  / 
( ( abs `  A
) ^ k ) ) )
97 elrp 9449 . . . . . . . . 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 9449 . . . . . . . . 9  |-  ( ( ( abs `  A
) ^ k )  e.  RR+  <->  ( ( ( abs `  A ) ^ k )  e.  RR  /\  0  < 
( ( abs `  A
) ^ k ) ) )
99 lerec2 8816 . . . . . . . . 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 634 . . . . . . 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 9463 . . . . . . . 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 8890 . . . . . . . 8  |-  ( k  e.  NN  ->  k  e.  CC )
106 nnne0 8911 . . . . . . . 8  |-  ( k  e.  NN  ->  k  =/=  0 )
107105, 106jca 511 . . . . . . 7  |-  ( k  e.  NN  ->  (
k  e.  CC  /\  k  =/=  0 ) )
108 recdiv2 8721 . . . . . . 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 3610 . . . . 5  |-  ( ( ( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( abs `  A
) ^ k )  <_  ( ( 1  /  ( ( 1  /  ( abs `  A
) )  -  1 ) )  /  k
) )
111110, 63, 553brtr4d 3614 . . . 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 9458 . . . . 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 10789 . . 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 10128 . . . . . . 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 2136 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( n  e.  NN0  |->  ( A ^ n ) ) `
 k )  e.  CC )
123 absexp 10578 . . . . . . 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 5045 . . . . . 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 2105 . . . . 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 10745 . . . 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 2255 1  |-  ( ph  ->  ( n  e.  NN0  |->  ( A ^ n ) )  ~~>  0 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 174    /\ wa 356    = wceq 1518    e. wcel 1520    =/= wne 2180   _Vcvv 2473   class class class wbr 3584    e. cmpt 3638   ` cfv 4266  (class class class)co 5356   CCcc 8151   RRcr 8152   0cc0 8153   1c1 8154    + caddc 8156    x. cmul 8158    <_ cle 8266    < clt 8270    - cmin 8389    / cdiv 8391   NNcn 8392   NN0cn0 8393   ZZcz 8394   RR+crp 8396   ^cexp 10111   abscabs 10485    ~~> cli 10668
This theorem is referenced by:  explecnv  10985  geolim  10988  geo2lim  10992  iscmet3lem3  16858  mbfi1fseqlem6  17217  geomcau  23542
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1440  ax-6 1441  ax-7 1442  ax-gen 1443  ax-8 1522  ax-11 1523  ax-13 1524  ax-14 1525  ax-17 1527  ax-12o 1560  ax-10 1574  ax-9 1580  ax-4 1587  ax-16 1773  ax-ext 2044  ax-rep 3689  ax-sep 3699  ax-nul 3707  ax-pow 3743  ax-pr 3767  ax-un 4059  ax-cnex 8208  ax-resscn 8209  ax-1cn 8210  ax-icn 8211  ax-addcl 8212  ax-addrcl 8213  ax-mulcl 8214  ax-mulrcl 8215  ax-mulcom 8216  ax-addass 8217  ax-mulass 8218  ax-distr 8219  ax-i2m1 8220  ax-1ne0 8221  ax-1rid 8222  ax-rnegex 8223  ax-rrecex 8224  ax-cnre 8225  ax-pre-lttri 8226  ax-pre-lttrn 8227  ax-pre-ltadd 8228  ax-pre-mulgt0 8229  ax-pre-sup 8230
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-3or 895  df-3an 896  df-tru 1257  df-ex 1445  df-sb 1734  df-eu 1956  df-mo 1957  df-clab 2050  df-cleq 2055  df-clel 2058  df-ne 2182  df-nel 2183  df-ral 2276  df-rex 2277  df-reu 2278  df-rab 2279  df-v 2475  df-sbc 2649  df-csb 2731  df-dif 2794  df-un 2796  df-in 2798  df-ss 2802  df-pss 2804  df-nul 3071  df-if 3180  df-pw 3241  df-sn 3259  df-pr 3260  df-tp 3261  df-op 3262  df-uni 3423  df-iun 3500  df-br 3585  df-opab 3639  df-mpt 3640  df-tr 3672  df-eprel 3854  df-id 3858  df-po 3863  df-so 3864  df-fr 3901  df-we 3903  df-ord 3944  df-on 3945  df-lim 3946  df-suc 3947  df-om 4222  df-xp 4268  df-rel 4269  df-cnv 4270  df-co 4271  df-dm 4272  df-rn 4273  df-res 4274  df-ima 4275  df-fun 4276  df-fn 4277  df-f 4278  df-f1 4279  df-fo 4280  df-f1o 4281  df-fv 4282  df-ov 5359  df-oprab 5360  df-mpt2 5361  df-2nd 5611  df-iota 5766  df-recs 5839  df-rdg 5874  df-er 6111  df-pm 6216  df-en 6298  df-dom 6299  df-sdom 6300  df-riota 6464  df-sup 6672  df-pnf 8271  df-mnf 8272  df-xr 8273  df-ltxr 8274  df-le 8275  df-sub 8408  df-neg 8409  df-div 8640  df-n 8883  df-2 8930  df-3 8931  df-n0 9076  df-z 9128  df-uz 9326  df-rp 9448  df-fl 9943  df-seq 10054  df-exp 10112  df-cj 10388  df-re 10389  df-im 10390  df-sqr 10486  df-abs 10487  df-clim 10671  df-rlim 10672
Copyright terms: Public domain