This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem expcnv

Description: A sequence of powers of a complex number A with absolute value less than 1 converges to zero. (Contributed by NM, 8-May-2006) (Proof shortened by Mario Carneiro, 26-Apr-2014)

Ref Expression
Hypotheses expcnv.1 
|- ( ph -> A e. CC )
expcnv.2 
|- ( ph -> ( abs ` A ) < 1 )
Assertion expcnv 
|- ( ph -> ( n e. NN0 |-> ( A ^ n ) ) ~~> 0 )

Proof

Step Hyp Ref Expression
1 expcnv.1 
 |-  ( ph -> A e. CC )
2 expcnv.2 
 |-  ( ph -> ( abs ` A ) < 1 )
3 nnuz 
 |-  NN = ( ZZ>= ` 1 )
4 1zzd 
 |-  ( ( ph /\ A = 0 ) -> 1 e. ZZ )
5 nn0ex 
 |-  NN0 e. _V
6 5 mptex 
 |-  ( n e. NN0 |-> ( A ^ n ) ) e. _V
7 6 a1i 
 |-  ( ( ph /\ A = 0 ) -> ( n e. NN0 |-> ( A ^ n ) ) e. _V )
8 0cnd 
 |-  ( ( ph /\ A = 0 ) -> 0 e. CC )
9 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
10 oveq2 
 |-  ( n = k -> ( A ^ n ) = ( A ^ k ) )
11 eqid 
 |-  ( n e. NN0 |-> ( A ^ n ) ) = ( n e. NN0 |-> ( A ^ n ) )
12 ovex 
 |-  ( A ^ k ) e. _V
13 10 11 12 fvmpt 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = ( A ^ k ) )
14 9 13 syl 
 |-  ( k e. NN -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = ( A ^ k ) )
15 simpr 
 |-  ( ( ph /\ A = 0 ) -> A = 0 )
16 15 oveq1d 
 |-  ( ( ph /\ A = 0 ) -> ( A ^ k ) = ( 0 ^ k ) )
17 14 16 sylan9eqr 
 |-  ( ( ( ph /\ A = 0 ) /\ k e. NN ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = ( 0 ^ k ) )
18 0exp 
 |-  ( k e. NN -> ( 0 ^ k ) = 0 )
19 18 adantl 
 |-  ( ( ( ph /\ A = 0 ) /\ k e. NN ) -> ( 0 ^ k ) = 0 )
20 17 19 eqtrd 
 |-  ( ( ( ph /\ A = 0 ) /\ k e. NN ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = 0 )
21 3 4 7 8 20 climconst 
 |-  ( ( ph /\ A = 0 ) -> ( n e. NN0 |-> ( A ^ n ) ) ~~> 0 )
22 1zzd 
 |-  ( ( ph /\ A =/= 0 ) -> 1 e. ZZ )
23 2 adantr 
 |-  ( ( ph /\ A =/= 0 ) -> ( abs ` A ) < 1 )
24 absrpcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR+ )
25 1 24 sylan 
 |-  ( ( ph /\ A =/= 0 ) -> ( abs ` A ) e. RR+ )
26 25 reclt1d 
 |-  ( ( ph /\ A =/= 0 ) -> ( ( abs ` A ) < 1 <-> 1 < ( 1 / ( abs ` A ) ) ) )
27 23 26 mpbid 
 |-  ( ( ph /\ A =/= 0 ) -> 1 < ( 1 / ( abs ` A ) ) )
28 1re 
 |-  1 e. RR
29 25 rpreccld 
 |-  ( ( ph /\ A =/= 0 ) -> ( 1 / ( abs ` A ) ) e. RR+ )
30 29 rpred 
 |-  ( ( ph /\ A =/= 0 ) -> ( 1 / ( abs ` A ) ) e. RR )
31 difrp 
 |-  ( ( 1 e. RR /\ ( 1 / ( abs ` A ) ) e. RR ) -> ( 1 < ( 1 / ( abs ` A ) ) <-> ( ( 1 / ( abs ` A ) ) - 1 ) e. RR+ ) )
32 28 30 31 sylancr 
 |-  ( ( ph /\ A =/= 0 ) -> ( 1 < ( 1 / ( abs ` A ) ) <-> ( ( 1 / ( abs ` A ) ) - 1 ) e. RR+ ) )
33 27 32 mpbid 
 |-  ( ( ph /\ A =/= 0 ) -> ( ( 1 / ( abs ` A ) ) - 1 ) e. RR+ )
34 33 rpreccld 
 |-  ( ( ph /\ A =/= 0 ) -> ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) e. RR+ )
35 34 rpcnd 
 |-  ( ( ph /\ A =/= 0 ) -> ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) e. CC )
36 divcnv 
 |-  ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) e. CC -> ( n e. NN |-> ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) / n ) ) ~~> 0 )
37 35 36 syl 
 |-  ( ( ph /\ A =/= 0 ) -> ( n e. NN |-> ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) / n ) ) ~~> 0 )
38 nnex 
 |-  NN e. _V
39 38 mptex 
 |-  ( n e. NN |-> ( ( abs ` A ) ^ n ) ) e. _V
40 39 a1i 
 |-  ( ( ph /\ A =/= 0 ) -> ( n e. NN |-> ( ( abs ` A ) ^ n ) ) e. _V )
41 oveq2 
 |-  ( n = k -> ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) / n ) = ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) / k ) )
42 eqid 
 |-  ( n e. NN |-> ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) / n ) ) = ( n e. NN |-> ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) / n ) )
43 ovex 
 |-  ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) / k ) e. _V
44 41 42 43 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) / n ) ) ` k ) = ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) / k ) )
45 44 adantl 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) / n ) ) ` k ) = ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) / k ) )
46 34 rpred 
 |-  ( ( ph /\ A =/= 0 ) -> ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) e. RR )
47 nndivre 
 |-  ( ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) e. RR /\ k e. NN ) -> ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) / k ) e. RR )
48 46 47 sylan 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) / k ) e. RR )
49 45 48 eqeltrd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) / n ) ) ` k ) e. RR )
50 oveq2 
 |-  ( n = k -> ( ( abs ` A ) ^ n ) = ( ( abs ` A ) ^ k ) )
51 eqid 
 |-  ( n e. NN |-> ( ( abs ` A ) ^ n ) ) = ( n e. NN |-> ( ( abs ` A ) ^ n ) )
52 ovex 
 |-  ( ( abs ` A ) ^ k ) e. _V
53 50 51 52 fvmpt 
 |-  ( k e. NN -> ( ( n e. NN |-> ( ( abs ` A ) ^ n ) ) ` k ) = ( ( abs ` A ) ^ k ) )
54 53 adantl 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( abs ` A ) ^ n ) ) ` k ) = ( ( abs ` A ) ^ k ) )
55 nnz 
 |-  ( k e. NN -> k e. ZZ )
56 rpexpcl 
 |-  ( ( ( abs ` A ) e. RR+ /\ k e. ZZ ) -> ( ( abs ` A ) ^ k ) e. RR+ )
57 25 55 56 syl2an 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( abs ` A ) ^ k ) e. RR+ )
58 54 57 eqeltrd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( abs ` A ) ^ n ) ) ` k ) e. RR+ )
59 58 rpred 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( abs ` A ) ^ n ) ) ` k ) e. RR )
60 nnrp 
 |-  ( k e. NN -> k e. RR+ )
61 rpmulcl 
 |-  ( ( ( ( 1 / ( abs ` A ) ) - 1 ) e. RR+ /\ k e. RR+ ) -> ( ( ( 1 / ( abs ` A ) ) - 1 ) x. k ) e. RR+ )
62 33 60 61 syl2an 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( ( 1 / ( abs ` A ) ) - 1 ) x. k ) e. RR+ )
63 62 rpred 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( ( 1 / ( abs ` A ) ) - 1 ) x. k ) e. RR )
64 peano2re 
 |-  ( ( ( ( 1 / ( abs ` A ) ) - 1 ) x. k ) e. RR -> ( ( ( ( 1 / ( abs ` A ) ) - 1 ) x. k ) + 1 ) e. RR )
65 63 64 syl 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( ( ( 1 / ( abs ` A ) ) - 1 ) x. k ) + 1 ) e. RR )
66 rpexpcl 
 |-  ( ( ( 1 / ( abs ` A ) ) e. RR+ /\ k e. ZZ ) -> ( ( 1 / ( abs ` A ) ) ^ k ) e. RR+ )
67 29 55 66 syl2an 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( 1 / ( abs ` A ) ) ^ k ) e. RR+ )
68 67 rpred 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( 1 / ( abs ` A ) ) ^ k ) e. RR )
69 63 lep1d 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( ( 1 / ( abs ` A ) ) - 1 ) x. k ) <_ ( ( ( ( 1 / ( abs ` A ) ) - 1 ) x. k ) + 1 ) )
70 30 adantr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( 1 / ( abs ` A ) ) e. RR )
71 9 adantl 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> k e. NN0 )
72 29 rpge0d 
 |-  ( ( ph /\ A =/= 0 ) -> 0 <_ ( 1 / ( abs ` A ) ) )
73 72 adantr 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> 0 <_ ( 1 / ( abs ` A ) ) )
74 bernneq2 
 |-  ( ( ( 1 / ( abs ` A ) ) e. RR /\ k e. NN0 /\ 0 <_ ( 1 / ( abs ` A ) ) ) -> ( ( ( ( 1 / ( abs ` A ) ) - 1 ) x. k ) + 1 ) <_ ( ( 1 / ( abs ` A ) ) ^ k ) )
75 70 71 73 74 syl3anc 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( ( ( 1 / ( abs ` A ) ) - 1 ) x. k ) + 1 ) <_ ( ( 1 / ( abs ` A ) ) ^ k ) )
76 63 65 68 69 75 letrd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( ( 1 / ( abs ` A ) ) - 1 ) x. k ) <_ ( ( 1 / ( abs ` A ) ) ^ k ) )
77 25 rpcnne0d 
 |-  ( ( ph /\ A =/= 0 ) -> ( ( abs ` A ) e. CC /\ ( abs ` A ) =/= 0 ) )
78 exprec 
 |-  ( ( ( abs ` A ) e. CC /\ ( abs ` A ) =/= 0 /\ k e. ZZ ) -> ( ( 1 / ( abs ` A ) ) ^ k ) = ( 1 / ( ( abs ` A ) ^ k ) ) )
79 78 3expa 
 |-  ( ( ( ( abs ` A ) e. CC /\ ( abs ` A ) =/= 0 ) /\ k e. ZZ ) -> ( ( 1 / ( abs ` A ) ) ^ k ) = ( 1 / ( ( abs ` A ) ^ k ) ) )
80 77 55 79 syl2an 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( 1 / ( abs ` A ) ) ^ k ) = ( 1 / ( ( abs ` A ) ^ k ) ) )
81 76 80 breqtrd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( ( 1 / ( abs ` A ) ) - 1 ) x. k ) <_ ( 1 / ( ( abs ` A ) ^ k ) ) )
82 62 57 81 lerec2d 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( abs ` A ) ^ k ) <_ ( 1 / ( ( ( 1 / ( abs ` A ) ) - 1 ) x. k ) ) )
83 33 rpcnne0d 
 |-  ( ( ph /\ A =/= 0 ) -> ( ( ( 1 / ( abs ` A ) ) - 1 ) e. CC /\ ( ( 1 / ( abs ` A ) ) - 1 ) =/= 0 ) )
84 nncn 
 |-  ( k e. NN -> k e. CC )
85 nnne0 
 |-  ( k e. NN -> k =/= 0 )
86 84 85 jca 
 |-  ( k e. NN -> ( k e. CC /\ k =/= 0 ) )
87 recdiv2 
 |-  ( ( ( ( ( 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 ) ) )
88 83 86 87 syl2an 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) / k ) = ( 1 / ( ( ( 1 / ( abs ` A ) ) - 1 ) x. k ) ) )
89 82 88 breqtrrd 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( abs ` A ) ^ k ) <_ ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) / k ) )
90 89 54 45 3brtr4d 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( abs ` A ) ^ n ) ) ` k ) <_ ( ( n e. NN |-> ( ( 1 / ( ( 1 / ( abs ` A ) ) - 1 ) ) / n ) ) ` k ) )
91 58 rpge0d 
 |-  ( ( ( ph /\ A =/= 0 ) /\ k e. NN ) -> 0 <_ ( ( n e. NN |-> ( ( abs ` A ) ^ n ) ) ` k ) )
92 3 22 37 40 49 59 90 91 climsqz2 
 |-  ( ( ph /\ A =/= 0 ) -> ( n e. NN |-> ( ( abs ` A ) ^ n ) ) ~~> 0 )
93 1zzd 
 |-  ( ph -> 1 e. ZZ )
94 6 a1i 
 |-  ( ph -> ( n e. NN0 |-> ( A ^ n ) ) e. _V )
95 39 a1i 
 |-  ( ph -> ( n e. NN |-> ( ( abs ` A ) ^ n ) ) e. _V )
96 9 adantl 
 |-  ( ( ph /\ k e. NN ) -> k e. NN0 )
97 96 13 syl 
 |-  ( ( ph /\ k e. NN ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = ( A ^ k ) )
98 expcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
99 1 9 98 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( A ^ k ) e. CC )
100 97 99 eqeltrd 
 |-  ( ( ph /\ k e. NN ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) e. CC )
101 absexp 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( abs ` ( A ^ k ) ) = ( ( abs ` A ) ^ k ) )
102 1 9 101 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( abs ` ( A ^ k ) ) = ( ( abs ` A ) ^ k ) )
103 97 fveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( abs ` ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) ) = ( abs ` ( A ^ k ) ) )
104 53 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( ( abs ` A ) ^ n ) ) ` k ) = ( ( abs ` A ) ^ k ) )
105 102 103 104 3eqtr4rd 
 |-  ( ( ph /\ k e. NN ) -> ( ( n e. NN |-> ( ( abs ` A ) ^ n ) ) ` k ) = ( abs ` ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) ) )
106 3 93 94 95 100 105 climabs0 
 |-  ( ph -> ( ( n e. NN0 |-> ( A ^ n ) ) ~~> 0 <-> ( n e. NN |-> ( ( abs ` A ) ^ n ) ) ~~> 0 ) )
107 106 biimpar 
 |-  ( ( ph /\ ( n e. NN |-> ( ( abs ` A ) ^ n ) ) ~~> 0 ) -> ( n e. NN0 |-> ( A ^ n ) ) ~~> 0 )
108 92 107 syldan 
 |-  ( ( ph /\ A =/= 0 ) -> ( n e. NN0 |-> ( A ^ n ) ) ~~> 0 )
109 21 108 pm2.61dane 
 |-  ( ph -> ( n e. NN0 |-> ( A ^ n ) ) ~~> 0 )