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

Theorem expcnv 10898
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 9337 . . 3  |-  NN  =  ( ZZ>= `  1 )
2 1z 9136 . . . 4  |-  1  e.  ZZ
32a1i 10 . . 3  |-  ( ( ph  /\  A  =  0 )  ->  1  e.  ZZ )
4 nn0ex 9061 . . . . 5  |-  NN0  e.  _V
54mptex 5190 . . . 4  |-  ( n  e.  NN0  |->  ( A ^
n ) )  e. 
_V
65a1i 10 . . 3  |-  ( ( ph  /\  A  =  0 )  ->  ( n  e.  NN0  |->  ( A ^
n ) )  e. 
_V )
7 0cn 8240 . . . 4  |-  0  e.  CC
87a1i 10 . . 3  |-  ( ( ph  /\  A  =  0 )  ->  0  e.  CC )
9 nnnn0 9062 . . . . . 6  |-  ( k  e.  NN  ->  k  e.  NN0 )
10 oveq2 5362 . . . . . . 7  |-  ( n  =  k  ->  ( A ^ n )  =  ( A ^ k
) )
11 eqid 2082 . . . . . . 7  |-  ( n  e.  NN0  |->  ( A ^
n ) )  =  ( n  e.  NN0  |->  ( A ^ n ) )
12 ovex 5378 . . . . . . 7  |-  ( A ^ k )  e. 
_V
1310, 11, 12fvmpt 5116 . . . . . 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 441 . . . . . 6  |-  ( ( ph  /\  A  =  0 )  ->  A  = 
0 )
1615oveq1d 5368 . . . . 5  |-  ( ( ph  /\  A  =  0 )  ->  ( A ^ k )  =  ( 0 ^ k
) )
1714, 16sylan9eqr 2136 . . . 4  |-  ( (
( ph  /\  A  =  0 )  /\  k  e.  NN )  ->  (
( n  e.  NN0  |->  ( A ^ n ) ) `  k )  =  ( 0 ^ k ) )
18 0exp 10108 . . . . 5  |-  ( k  e.  NN  ->  ( 0 ^ k )  =  0 )
1918adantl 446 . . . 4  |-  ( (
( ph  /\  A  =  0 )  /\  k  e.  NN )  ->  (
0 ^ k )  =  0 )
2017, 19eqtrd 2114 . . 3  |-  ( (
( ph  /\  A  =  0 )  /\  k  e.  NN )  ->  (
( n  e.  NN0  |->  ( A ^ n ) ) `  k )  =  0 )
211, 3, 6, 8, 20climconst 10647 . 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 445 . . . . . . . . . 10  |-  ( ( ph  /\  A  =/=  0
)  ->  ( abs `  A )  <  1
)
25 expcnv.1 . . . . . . . . . . . 12  |-  ( ph  ->  A  e.  CC )
26 absrpcl 10509 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  A  =/=  0 )  ->  ( abs `  A )  e.  RR+ )
2725, 26sylan 451 . . . . . . . . . . 11  |-  ( ( ph  /\  A  =/=  0
)  ->  ( abs `  A )  e.  RR+ )
28 elrp 9428 . . . . . . . . . . . 12  |-  ( ( abs `  A )  e.  RR+ 
<->  ( ( abs `  A
)  e.  RR  /\  0  <  ( abs `  A
) ) )
29 reclt1 8805 . . . . . . . . . . . 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 8248 . . . . . . . . . 10  |-  1  e.  RR
34 rpreccl 9448 . . . . . . . . . . . 12  |-  ( ( abs `  A )  e.  RR+  ->  ( 1  / 
( abs `  A
) )  e.  RR+ )
3527, 34syl 15 . . . . . . . . . . 11  |-  ( ( ph  /\  A  =/=  0
)  ->  ( 1  /  ( abs `  A
) )  e.  RR+ )
36 rpre 9431 . . . . . . . . . . 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 9457 . . . . . . . . . 10  |-  ( (
1  e.  RR  /\  ( 1  /  ( abs `  A ) )  e.  RR )  -> 
( 1  <  (
1  /  ( abs `  A ) )  <->  ( (
1  /  ( abs `  A ) )  - 
1 )  e.  RR+ ) )
3933, 37, 38sylancr 640 . . . . . . . . 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 9448 . . . . . . . 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 9431 . . . . . . 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 8229 . . . . 5  |-  ( ( ph  /\  A  =/=  0
)  ->  ( 1  /  ( ( 1  /  ( abs `  A
) )  -  1 ) )  e.  CC )
46 divcnv 10889 . . . . 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 8868 . . . . . 6  |-  NN  e.  _V
4948mptex 5190 . . . . 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 5362 . . . . . . 7  |-  ( n  =  k  ->  ( ( 1  /  ( ( 1  /  ( abs `  A ) )  - 
1 ) )  /  n )  =  ( ( 1  /  (
( 1  /  ( abs `  A ) )  -  1 ) )  /  k ) )
52 eqid 2082 . . . . . . 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 5116 . . . . . 6  |-  ( k  e.  NN  ->  ( (
n  e.  NN  |->  ( ( 1  /  (
( 1  /  ( abs `  A ) )  -  1 ) )  /  n ) ) `
 k )  =  ( ( 1  / 
( ( 1  / 
( abs `  A
) )  -  1 ) )  /  k
) )
5554adantl 446 . . . . 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 8894 . . . . . 6  |-  ( (
( 1  /  (
( 1  /  ( abs `  A ) )  -  1 ) )  e.  RR  /\  k  e.  NN )  ->  (
( 1  /  (
( 1  /  ( abs `  A ) )  -  1 ) )  /  k )  e.  RR )
5744, 56sylan 451 . . . . 5  |-  ( (
( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( 1  /  (
( 1  /  ( abs `  A ) )  -  1 ) )  /  k )  e.  RR )
5855, 57eqeltrd 2155 . . . 4  |-  ( (
( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( ( 1  / 
( ( 1  / 
( abs `  A
) )  -  1 ) )  /  n
) ) `  k
)  e.  RR )
59 oveq2 5362 . . . . . . . 8  |-  ( n  =  k  ->  ( ( abs `  A ) ^ n )  =  ( ( abs `  A
) ^ k ) )
60 eqid 2082 . . . . . . . 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 5116 . . . . . . 7  |-  ( k  e.  NN  ->  ( (
n  e.  NN  |->  ( ( abs `  A
) ^ n ) ) `  k )  =  ( ( abs `  A ) ^ k
) )
6362adantl 446 . . . . . 6  |-  ( (
( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( ( abs `  A
) ^ n ) ) `  k )  =  ( ( abs `  A ) ^ k
) )
64 nnz 9128 . . . . . . 7  |-  ( k  e.  NN  ->  k  e.  ZZ )
65 rpexpcl 10093 . . . . . . 7  |-  ( (
( abs `  A
)  e.  RR+  /\  k  e.  ZZ )  ->  (
( abs `  A
) ^ k )  e.  RR+ )
6627, 64, 65syl2an 457 . . . . . 6  |-  ( (
( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( abs `  A
) ^ k )  e.  RR+ )
6763, 66eqeltrd 2155 . . . . 5  |-  ( (
( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( ( abs `  A
) ^ n ) ) `  k )  e.  RR+ )
68 rpre 9431 . . . . 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 9434 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  k  e.  RR+ )
71 rpmulcl 9446 . . . . . . . . . . 11  |-  ( (
( ( 1  / 
( abs `  A
) )  -  1 )  e.  RR+  /\  k  e.  RR+ )  ->  (
( ( 1  / 
( abs `  A
) )  -  1 )  x.  k )  e.  RR+ )
7240, 70, 71syl2an 457 . . . . . . . . . 10  |-  ( (
( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( ( 1  / 
( abs `  A
) )  -  1 )  x.  k )  e.  RR+ )
73 rpre 9431 . . . . . . . . . 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 8350 . . . . . . . . . 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 10093 . . . . . . . . . . 11  |-  ( (
( 1  /  ( abs `  A ) )  e.  RR+  /\  k  e.  ZZ )  ->  (
( 1  /  ( abs `  A ) ) ^ k )  e.  RR+ )
7835, 64, 77syl2an 457 . . . . . . . . . 10  |-  ( (
( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( 1  /  ( abs `  A ) ) ^ k )  e.  RR+ )
79 rpre 9431 . . . . . . . . . 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 8726 . . . . . . . . . 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 445 . . . . . . . . . 10  |-  ( (
( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
1  /  ( abs `  A ) )  e.  RR )
849adantl 446 . . . . . . . . . 10  |-  ( (
( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  k  e.  NN0 )
85 rpge0 9437 . . . . . . . . . . . 12  |-  ( (
1  /  ( abs `  A ) )  e.  RR+  ->  0  <_  (
1  /  ( abs `  A ) ) )
8635, 85syl 15 . . . . . . . . . . 11  |-  ( ( ph  /\  A  =/=  0
)  ->  0  <_  ( 1  /  ( abs `  A ) ) )
8786adantr 445 . . . . . . . . . 10  |-  ( (
( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  0  <_  ( 1  /  ( abs `  A ) ) )
88 bernneq2 10195 . . . . . . . . . 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 1149 . . . . . . . . 9  |-  ( (
( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( ( ( 1  /  ( abs `  A
) )  -  1 )  x.  k )  +  1 )  <_ 
( ( 1  / 
( abs `  A
) ) ^ k
) )
9074, 76, 80, 82, 89letrd 8297 . . . . . . . 8  |-  ( (
( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( ( 1  / 
( abs `  A
) )  -  1 )  x.  k )  <_  ( ( 1  /  ( abs `  A
) ) ^ k
) )
91 rpcnne0 9442 . . . . . . . . . 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 10114 . . . . . . . . . 10  |-  ( (
( abs `  A
)  e.  CC  /\  ( abs `  A )  =/=  0  /\  k  e.  ZZ )  ->  (
( 1  /  ( abs `  A ) ) ^ k )  =  ( 1  /  (
( abs `  A
) ^ k ) ) )
94933expa 1119 . . . . . . . . 9  |-  ( (
( ( abs `  A
)  e.  CC  /\  ( abs `  A )  =/=  0 )  /\  k  e.  ZZ )  ->  ( ( 1  / 
( abs `  A
) ) ^ k
)  =  ( 1  /  ( ( abs `  A ) ^ k
) ) )
9592, 64, 94syl2an 457 . . . . . . . 8  |-  ( (
( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( 1  /  ( abs `  A ) ) ^ k )  =  ( 1  /  (
( abs `  A
) ^ k ) ) )
9690, 95breqtrd 3624 . . . . . . 7  |-  ( (
( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( ( 1  / 
( abs `  A
) )  -  1 )  x.  k )  <_  ( 1  / 
( ( abs `  A
) ^ k ) ) )
97 elrp 9428 . . . . . . . . 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 9428 . . . . . . . . 9  |-  ( (
( abs `  A
) ^ k )  e.  RR+  <->  ( ( ( abs `  A ) ^ k )  e.  RR  /\  0  < 
( ( abs `  A
) ^ k ) ) )
99 lerec2 8796 . . . . . . . . 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 459 . . . . . . . 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 638 . . . . . . 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 9442 . . . . . . . 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 8870 . . . . . . . 8  |-  ( k  e.  NN  ->  k  e.  CC )
106 nnne0 8891 . . . . . . . 8  |-  ( k  e.  NN  ->  k  =/=  0 )
107105, 106jca 514 . . . . . . 7  |-  ( k  e.  NN  ->  ( k  e.  CC  /\  k  =/=  0 ) )
108 recdiv2 8707 . . . . . . 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 457 . . . . . 6  |-  ( (
( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( 1  /  (
( 1  /  ( abs `  A ) )  -  1 ) )  /  k )  =  ( 1  /  (
( ( 1  / 
( abs `  A
) )  -  1 )  x.  k ) ) )
110102, 109breqtrrd 3626 . . . . 5  |-  ( (
( ph  /\  A  =/=  0 )  /\  k  e.  NN )  ->  (
( abs `  A
) ^ k )  <_  ( ( 1  /  ( ( 1  /  ( abs `  A
) )  -  1 ) )  /  k
) )
111110, 63, 553brtr4d 3630 . . . 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 9437 . . . . 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 10701 . . 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 446 . . . . . . 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 10092 . . . . . . 7  |-  ( ( A  e.  CC  /\  k  e.  NN0 )  ->  ( A ^ k )  e.  CC )
12125, 9, 120syl2an 457 . . . . . 6  |-  ( ( ph  /\  k  e.  NN )  ->  ( A ^
k )  e.  CC )
122119, 121eqeltrd 2155 . . . . 5  |-  ( ( ph  /\  k  e.  NN )  ->  ( ( n  e.  NN0  |->  ( A ^ n ) ) `
 k )  e.  CC )
123 absexp 10524 . . . . . . 7  |-  ( ( A  e.  CC  /\  k  e.  NN0 )  ->  ( abs `  ( A ^
k ) )  =  ( ( abs `  A
) ^ k ) )
12425, 9, 123syl2an 457 . . . . . 6  |-  ( ( ph  /\  k  e.  NN )  ->  ( abs `  ( A ^ k ) )  =  ( ( abs `  A ) ^ k
) )
125119fveq2d 5046 . . . . . 6  |-  ( ( ph  /\  k  e.  NN )  ->  ( abs `  (
( n  e.  NN0  |->  ( A ^ n ) ) `  k ) )  =  ( abs `  ( A ^ k
) ) )
12662adantl 446 . . . . . 6  |-  ( ( ph  /\  k  e.  NN )  ->  ( ( n  e.  NN  |->  ( ( abs `  A ) ^ n ) ) `
 k )  =  ( ( abs `  A
) ^ k ) )
127124, 125, 1263eqtr4rd 2125 . . . . 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 10676 . . . 4  |-  ( ph  ->  ( ( n  e. 
NN0  |->  ( A ^
n ) )  ~~>  0  <->  (
n  e.  NN  |->  ( ( abs `  A
) ^ n ) )  ~~>  0 ) )
129128biimpar 465 . . 3  |-  ( ( ph  /\  ( n  e.  NN  |->  ( ( abs `  A ) ^ n
) )  ~~>  0 )  ->  ( n  e. 
NN0  |->  ( A ^
n ) )  ~~>  0 )
130114, 129syldan 450 . 2  |-  ( ( ph  /\  A  =/=  0
)  ->  ( n  e.  NN0  |->  ( A ^
n ) )  ~~>  0 )
13121, 130pm2.61dane 2274 1  |-  ( ph  ->  ( n  e.  NN0  |->  ( A ^ n ) )  ~~>  0 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 174    /\ wa 357    = wceq 1536    e. wcel 1538    =/= wne 2199   _Vcvv 2492   class class class wbr 3600    e. cmpt 3654   ` cfv 4287  (class class class)co 5354   CCcc 8135   RRcr 8136   0cc0 8137   1c1 8138    + caddc 8140    x. cmul 8142    <_ cle 8250    < clt 8254    - cmin 8373    / cdiv 8375   NNcn 8376   NN0cn0 8377   ZZcz 8378   RR+crp 8380   ^cexp 10075   abscabs 10432    ~~> cli 10610
This theorem is referenced by:  explecnv  10899  geolim  10901  geo2lim  10905  iscmet3lem3  16432  mbfi1fseqlem6  16791  geomcau  22923
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1451  ax-6 1452  ax-7 1453  ax-gen 1454  ax-8 1540  ax-11 1541  ax-13 1542  ax-14 1543  ax-17 1545  ax-12o 1578  ax-10 1592  ax-9 1598  ax-4 1606  ax-16 1793  ax-ext 2064  ax-rep 3705  ax-sep 3715  ax-nul 3723  ax-pow 3759  ax-pr 3783  ax-un 4075  ax-cnex 8192  ax-resscn 8193  ax-1cn 8194  ax-icn 8195  ax-addcl 8196  ax-addrcl 8197  ax-mulcl 8198  ax-mulrcl 8199  ax-mulcom 8200  ax-addass 8201  ax-mulass 8202  ax-distr 8203  ax-i2m1 8204  ax-1ne0 8205  ax-1rid 8206  ax-rnegex 8207  ax-rrecex 8208  ax-cnre 8209  ax-pre-lttri 8210  ax-pre-lttrn 8211  ax-pre-ltadd 8212  ax-pre-mulgt0 8213  ax-pre-sup 8214
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 904  df-3an 905  df-tru 1268  df-ex 1456  df-sb 1754  df-eu 1976  df-mo 1977  df-clab 2070  df-cleq 2075  df-clel 2078  df-ne 2201  df-nel 2202  df-ral 2295  df-rex 2296  df-reu 2297  df-rab 2298  df-v 2494  df-sbc 2668  df-csb 2750  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-pss 2823  df-nul 3089  df-if 3199  df-pw 3260  df-sn 3278  df-pr 3279  df-tp 3280  df-op 3281  df-uni 3439  df-iun 3516  df-br 3601  df-opab 3655  df-mpt 3656  df-tr 3688  df-eprel 3870  df-id 3874  df-po 3879  df-so 3880  df-fr 3917  df-we 3919  df-ord 3960  df-on 3961  df-lim 3962  df-suc 3963  df-om 4243  df-xp 4289  df-rel 4290  df-cnv 4291  df-co 4292  df-dm 4293  df-rn 4294  df-res 4295  df-ima 4296  df-fun 4297  df-fn 4298  df-f 4299  df-f1 4300  df-fo 4301  df-f1o 4302  df-fv 4303  df-ov 5357  df-oprab 5358  df-mpt2 5359  df-2nd 5609  df-iota 5762  df-recs 5835  df-rdg 5870  df-er 6102  df-pm 6208  df-en 6289  df-dom 6290  df-sdom 6291  df-riota 6455  df-sup 6656  df-pnf 8255  df-mnf 8256  df-xr 8257  df-ltxr 8258  df-le 8259  df-sub 8392  df-neg 8393  df-div 8621  df-n 8863  df-2 8910  df-3 8911  df-n0 9056  df-z 9108  df-uz 9305  df-rp 9427  df-fl 9917  df-seq 10021  df-exp 10076  df-cj 10335  df-re 10336  df-im 10337  df-sqr 10433  df-abs 10434  df-clim 10613  df-rlim 10614
Copyright terms: Public domain