Step |
Hyp |
Ref |
Expression |
1 |
|
nn0uz |
|- NN0 = ( ZZ>= ` 0 ) |
2 |
|
1nn0 |
|- 1 e. NN0 |
3 |
2
|
a1i |
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 1 e. NN0 ) |
4 |
|
oveq2 |
|- ( n = k -> ( ( abs ` A ) ^ n ) = ( ( abs ` A ) ^ k ) ) |
5 |
|
eqid |
|- ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) = ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) |
6 |
|
ovex |
|- ( ( abs ` A ) ^ k ) e. _V |
7 |
4 5 6
|
fvmpt |
|- ( k e. NN0 -> ( ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ` k ) = ( ( abs ` A ) ^ k ) ) |
8 |
7
|
adantl |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ` k ) = ( ( abs ` A ) ^ k ) ) |
9 |
|
abscl |
|- ( A e. CC -> ( abs ` A ) e. RR ) |
10 |
9
|
adantr |
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) e. RR ) |
11 |
|
reexpcl |
|- ( ( ( abs ` A ) e. RR /\ k e. NN0 ) -> ( ( abs ` A ) ^ k ) e. RR ) |
12 |
10 11
|
sylan |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( ( abs ` A ) ^ k ) e. RR ) |
13 |
8 12
|
eqeltrd |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ` k ) e. RR ) |
14 |
|
eqeq1 |
|- ( n = k -> ( n = 0 <-> k = 0 ) ) |
15 |
|
oveq2 |
|- ( n = k -> ( 1 / n ) = ( 1 / k ) ) |
16 |
14 15
|
ifbieq2d |
|- ( n = k -> if ( n = 0 , 0 , ( 1 / n ) ) = if ( k = 0 , 0 , ( 1 / k ) ) ) |
17 |
|
oveq2 |
|- ( n = k -> ( A ^ n ) = ( A ^ k ) ) |
18 |
16 17
|
oveq12d |
|- ( n = k -> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) = ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) |
19 |
|
eqid |
|- ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) = ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) |
20 |
|
ovex |
|- ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) e. _V |
21 |
18 19 20
|
fvmpt |
|- ( k e. NN0 -> ( ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ` k ) = ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) |
22 |
21
|
adantl |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ` k ) = ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) |
23 |
|
0cnd |
|- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) /\ k = 0 ) -> 0 e. CC ) |
24 |
|
nn0cn |
|- ( k e. NN0 -> k e. CC ) |
25 |
24
|
adantl |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> k e. CC ) |
26 |
|
neqne |
|- ( -. k = 0 -> k =/= 0 ) |
27 |
|
reccl |
|- ( ( k e. CC /\ k =/= 0 ) -> ( 1 / k ) e. CC ) |
28 |
25 26 27
|
syl2an |
|- ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) /\ -. k = 0 ) -> ( 1 / k ) e. CC ) |
29 |
23 28
|
ifclda |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> if ( k = 0 , 0 , ( 1 / k ) ) e. CC ) |
30 |
|
expcl |
|- ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC ) |
31 |
30
|
adantlr |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( A ^ k ) e. CC ) |
32 |
29 31
|
mulcld |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) e. CC ) |
33 |
22 32
|
eqeltrd |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ` k ) e. CC ) |
34 |
10
|
recnd |
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) e. CC ) |
35 |
|
absidm |
|- ( A e. CC -> ( abs ` ( abs ` A ) ) = ( abs ` A ) ) |
36 |
35
|
adantr |
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` ( abs ` A ) ) = ( abs ` A ) ) |
37 |
|
simpr |
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) < 1 ) |
38 |
36 37
|
eqbrtrd |
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` ( abs ` A ) ) < 1 ) |
39 |
34 38 8
|
geolim |
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ) ~~> ( 1 / ( 1 - ( abs ` A ) ) ) ) |
40 |
|
seqex |
|- seq 0 ( + , ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ) e. _V |
41 |
|
ovex |
|- ( 1 / ( 1 - ( abs ` A ) ) ) e. _V |
42 |
40 41
|
breldm |
|- ( seq 0 ( + , ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ) ~~> ( 1 / ( 1 - ( abs ` A ) ) ) -> seq 0 ( + , ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ) e. dom ~~> ) |
43 |
39 42
|
syl |
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ) e. dom ~~> ) |
44 |
|
1red |
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 1 e. RR ) |
45 |
|
elnnuz |
|- ( k e. NN <-> k e. ( ZZ>= ` 1 ) ) |
46 |
|
nnrecre |
|- ( k e. NN -> ( 1 / k ) e. RR ) |
47 |
46
|
adantl |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( 1 / k ) e. RR ) |
48 |
47
|
recnd |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( 1 / k ) e. CC ) |
49 |
|
nnnn0 |
|- ( k e. NN -> k e. NN0 ) |
50 |
49 31
|
sylan2 |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( A ^ k ) e. CC ) |
51 |
48 50
|
absmuld |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( abs ` ( ( 1 / k ) x. ( A ^ k ) ) ) = ( ( abs ` ( 1 / k ) ) x. ( abs ` ( A ^ k ) ) ) ) |
52 |
|
nnrp |
|- ( k e. NN -> k e. RR+ ) |
53 |
52
|
adantl |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> k e. RR+ ) |
54 |
53
|
rpreccld |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( 1 / k ) e. RR+ ) |
55 |
54
|
rpge0d |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> 0 <_ ( 1 / k ) ) |
56 |
47 55
|
absidd |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( abs ` ( 1 / k ) ) = ( 1 / k ) ) |
57 |
|
simpl |
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. CC ) |
58 |
|
absexp |
|- ( ( A e. CC /\ k e. NN0 ) -> ( abs ` ( A ^ k ) ) = ( ( abs ` A ) ^ k ) ) |
59 |
57 49 58
|
syl2an |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( abs ` ( A ^ k ) ) = ( ( abs ` A ) ^ k ) ) |
60 |
56 59
|
oveq12d |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( ( abs ` ( 1 / k ) ) x. ( abs ` ( A ^ k ) ) ) = ( ( 1 / k ) x. ( ( abs ` A ) ^ k ) ) ) |
61 |
51 60
|
eqtrd |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( abs ` ( ( 1 / k ) x. ( A ^ k ) ) ) = ( ( 1 / k ) x. ( ( abs ` A ) ^ k ) ) ) |
62 |
|
1red |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> 1 e. RR ) |
63 |
49 12
|
sylan2 |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( ( abs ` A ) ^ k ) e. RR ) |
64 |
50
|
absge0d |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> 0 <_ ( abs ` ( A ^ k ) ) ) |
65 |
64 59
|
breqtrd |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> 0 <_ ( ( abs ` A ) ^ k ) ) |
66 |
|
nnge1 |
|- ( k e. NN -> 1 <_ k ) |
67 |
66
|
adantl |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> 1 <_ k ) |
68 |
|
0lt1 |
|- 0 < 1 |
69 |
68
|
a1i |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> 0 < 1 ) |
70 |
|
nnre |
|- ( k e. NN -> k e. RR ) |
71 |
70
|
adantl |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> k e. RR ) |
72 |
|
nngt0 |
|- ( k e. NN -> 0 < k ) |
73 |
72
|
adantl |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> 0 < k ) |
74 |
|
lerec |
|- ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( k e. RR /\ 0 < k ) ) -> ( 1 <_ k <-> ( 1 / k ) <_ ( 1 / 1 ) ) ) |
75 |
62 69 71 73 74
|
syl22anc |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( 1 <_ k <-> ( 1 / k ) <_ ( 1 / 1 ) ) ) |
76 |
67 75
|
mpbid |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( 1 / k ) <_ ( 1 / 1 ) ) |
77 |
|
1div1e1 |
|- ( 1 / 1 ) = 1 |
78 |
76 77
|
breqtrdi |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( 1 / k ) <_ 1 ) |
79 |
47 62 63 65 78
|
lemul1ad |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( ( 1 / k ) x. ( ( abs ` A ) ^ k ) ) <_ ( 1 x. ( ( abs ` A ) ^ k ) ) ) |
80 |
61 79
|
eqbrtrd |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( abs ` ( ( 1 / k ) x. ( A ^ k ) ) ) <_ ( 1 x. ( ( abs ` A ) ^ k ) ) ) |
81 |
49 22
|
sylan2 |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ` k ) = ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) ) |
82 |
|
nnne0 |
|- ( k e. NN -> k =/= 0 ) |
83 |
82
|
adantl |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> k =/= 0 ) |
84 |
83
|
neneqd |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> -. k = 0 ) |
85 |
84
|
iffalsed |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> if ( k = 0 , 0 , ( 1 / k ) ) = ( 1 / k ) ) |
86 |
85
|
oveq1d |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( if ( k = 0 , 0 , ( 1 / k ) ) x. ( A ^ k ) ) = ( ( 1 / k ) x. ( A ^ k ) ) ) |
87 |
81 86
|
eqtrd |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ` k ) = ( ( 1 / k ) x. ( A ^ k ) ) ) |
88 |
87
|
fveq2d |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( abs ` ( ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ` k ) ) = ( abs ` ( ( 1 / k ) x. ( A ^ k ) ) ) ) |
89 |
49 8
|
sylan2 |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ` k ) = ( ( abs ` A ) ^ k ) ) |
90 |
89
|
oveq2d |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( 1 x. ( ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ` k ) ) = ( 1 x. ( ( abs ` A ) ^ k ) ) ) |
91 |
80 88 90
|
3brtr4d |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( abs ` ( ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ` k ) ) <_ ( 1 x. ( ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ` k ) ) ) |
92 |
45 91
|
sylan2br |
|- ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. ( ZZ>= ` 1 ) ) -> ( abs ` ( ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ` k ) ) <_ ( 1 x. ( ( n e. NN0 |-> ( ( abs ` A ) ^ n ) ) ` k ) ) ) |
93 |
1 3 13 33 43 44 92
|
cvgcmpce |
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ) e. dom ~~> ) |