Metamath Proof Explorer

Theorem geomulcvg

Description: The geometric series converges even if it is multiplied by k to result in the larger series k x. A ^ k . (Contributed by Mario Carneiro, 27-Mar-2015)

Ref Expression
Hypothesis geomulcvg.1 
|- F = ( k e. NN0 |-> ( k x. ( A ^ k ) ) )
Assertion geomulcvg 
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , F ) e. dom ~~> )

Proof

Step Hyp Ref Expression
1 geomulcvg.1 
 |-  F = ( k e. NN0 |-> ( k x. ( A ^ k ) ) )
2 elnn0 
 |-  ( k e. NN0 <-> ( k e. NN \/ k = 0 ) )
3 simpr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) -> A = 0 )
4 3 oveq1d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) -> ( A ^ k ) = ( 0 ^ k ) )
5 0exp 
 |-  ( k e. NN -> ( 0 ^ k ) = 0 )
6 4 5 sylan9eq 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) /\ k e. NN ) -> ( A ^ k ) = 0 )
7 6 oveq2d 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) /\ k e. NN ) -> ( k x. ( A ^ k ) ) = ( k x. 0 ) )
8 nncn 
 |-  ( k e. NN -> k e. CC )
9 8 adantl 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) /\ k e. NN ) -> k e. CC )
10 9 mul01d 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) /\ k e. NN ) -> ( k x. 0 ) = 0 )
11 7 10 eqtrd 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) /\ k e. NN ) -> ( k x. ( A ^ k ) ) = 0 )
12 simpr 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) /\ k = 0 ) -> k = 0 )
13 12 oveq1d 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) /\ k = 0 ) -> ( k x. ( A ^ k ) ) = ( 0 x. ( A ^ k ) ) )
14 simplll 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) /\ k = 0 ) -> A e. CC )
15 0nn0 
 |-  0 e. NN0
16 12 15 eqeltrdi 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) /\ k = 0 ) -> k e. NN0 )
17 14 16 expcld 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) /\ k = 0 ) -> ( A ^ k ) e. CC )
18 17 mul02d 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) /\ k = 0 ) -> ( 0 x. ( A ^ k ) ) = 0 )
19 13 18 eqtrd 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) /\ k = 0 ) -> ( k x. ( A ^ k ) ) = 0 )
20 11 19 jaodan 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) /\ ( k e. NN \/ k = 0 ) ) -> ( k x. ( A ^ k ) ) = 0 )
21 2 20 sylan2b 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) /\ k e. NN0 ) -> ( k x. ( A ^ k ) ) = 0 )
22 21 mpteq2dva 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) -> ( k e. NN0 |-> ( k x. ( A ^ k ) ) ) = ( k e. NN0 |-> 0 ) )
23 1 22 syl5eq 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) -> F = ( k e. NN0 |-> 0 ) )
24 fconstmpt 
 |-  ( NN0 X. { 0 } ) = ( k e. NN0 |-> 0 )
25 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
26 25 xpeq1i 
 |-  ( NN0 X. { 0 } ) = ( ( ZZ>= ` 0 ) X. { 0 } )
27 24 26 eqtr3i 
 |-  ( k e. NN0 |-> 0 ) = ( ( ZZ>= ` 0 ) X. { 0 } )
28 23 27 eqtrdi 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) -> F = ( ( ZZ>= ` 0 ) X. { 0 } ) )
29 28 seqeq3d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) -> seq 0 ( + , F ) = seq 0 ( + , ( ( ZZ>= ` 0 ) X. { 0 } ) ) )
30 0z 
 |-  0 e. ZZ
31 serclim0 
 |-  ( 0 e. ZZ -> seq 0 ( + , ( ( ZZ>= ` 0 ) X. { 0 } ) ) ~~> 0 )
32 30 31 ax-mp 
 |-  seq 0 ( + , ( ( ZZ>= ` 0 ) X. { 0 } ) ) ~~> 0
33 29 32 eqbrtrdi 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) -> seq 0 ( + , F ) ~~> 0 )
34 seqex 
 |-  seq 0 ( + , F ) e. _V
35 c0ex 
 |-  0 e. _V
36 34 35 breldm 
 |-  ( seq 0 ( + , F ) ~~> 0 -> seq 0 ( + , F ) e. dom ~~> )
37 33 36 syl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A = 0 ) -> seq 0 ( + , F ) e. dom ~~> )
38 1red 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) -> 1 e. RR )
39 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
40 39 adantr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) e. RR )
41 peano2re 
 |-  ( ( abs ` A ) e. RR -> ( ( abs ` A ) + 1 ) e. RR )
42 40 41 syl 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( abs ` A ) + 1 ) e. RR )
43 42 rehalfcld 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( ( abs ` A ) + 1 ) / 2 ) e. RR )
44 43 adantr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) -> ( ( ( abs ` A ) + 1 ) / 2 ) e. RR )
45 absrpcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR+ )
46 45 adantlr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) -> ( abs ` A ) e. RR+ )
47 44 46 rerpdivcld 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) -> ( ( ( ( abs ` A ) + 1 ) / 2 ) / ( abs ` A ) ) e. RR )
48 40 recnd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) e. CC )
49 48 mulid2d 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( 1 x. ( abs ` A ) ) = ( abs ` A ) )
50 simpr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) < 1 )
51 1re 
 |-  1 e. RR
52 avglt1 
 |-  ( ( ( abs ` A ) e. RR /\ 1 e. RR ) -> ( ( abs ` A ) < 1 <-> ( abs ` A ) < ( ( ( abs ` A ) + 1 ) / 2 ) ) )
53 40 51 52 sylancl 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( abs ` A ) < 1 <-> ( abs ` A ) < ( ( ( abs ` A ) + 1 ) / 2 ) ) )
54 50 53 mpbid 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) < ( ( ( abs ` A ) + 1 ) / 2 ) )
55 49 54 eqbrtrd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( 1 x. ( abs ` A ) ) < ( ( ( abs ` A ) + 1 ) / 2 ) )
56 55 adantr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) -> ( 1 x. ( abs ` A ) ) < ( ( ( abs ` A ) + 1 ) / 2 ) )
57 38 44 46 ltmuldivd 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) -> ( ( 1 x. ( abs ` A ) ) < ( ( ( abs ` A ) + 1 ) / 2 ) <-> 1 < ( ( ( ( abs ` A ) + 1 ) / 2 ) / ( abs ` A ) ) ) )
58 56 57 mpbid 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) -> 1 < ( ( ( ( abs ` A ) + 1 ) / 2 ) / ( abs ` A ) ) )
59 expmulnbnd 
 |-  ( ( 1 e. RR /\ ( ( ( ( abs ` A ) + 1 ) / 2 ) / ( abs ` A ) ) e. RR /\ 1 < ( ( ( ( abs ` A ) + 1 ) / 2 ) / ( abs ` A ) ) ) -> E. n e. NN0 A. k e. ( ZZ>= ` n ) ( 1 x. k ) < ( ( ( ( ( abs ` A ) + 1 ) / 2 ) / ( abs ` A ) ) ^ k ) )
60 38 47 58 59 syl3anc 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) -> E. n e. NN0 A. k e. ( ZZ>= ` n ) ( 1 x. k ) < ( ( ( ( ( abs ` A ) + 1 ) / 2 ) / ( abs ` A ) ) ^ k ) )
61 eluznn0 
 |-  ( ( n e. NN0 /\ k e. ( ZZ>= ` n ) ) -> k e. NN0 )
62 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
63 62 adantl 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ k e. NN0 ) -> k e. CC )
64 63 mulid2d 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ k e. NN0 ) -> ( 1 x. k ) = k )
65 43 recnd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( ( abs ` A ) + 1 ) / 2 ) e. CC )
66 65 ad2antrr 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ k e. NN0 ) -> ( ( ( abs ` A ) + 1 ) / 2 ) e. CC )
67 48 ad2antrr 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ k e. NN0 ) -> ( abs ` A ) e. CC )
68 46 adantr 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ k e. NN0 ) -> ( abs ` A ) e. RR+ )
69 68 rpne0d 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ k e. NN0 ) -> ( abs ` A ) =/= 0 )
70 simpr 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ k e. NN0 ) -> k e. NN0 )
71 66 67 69 70 expdivd 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ k e. NN0 ) -> ( ( ( ( ( abs ` A ) + 1 ) / 2 ) / ( abs ` A ) ) ^ k ) = ( ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) / ( ( abs ` A ) ^ k ) ) )
72 64 71 breq12d 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ k e. NN0 ) -> ( ( 1 x. k ) < ( ( ( ( ( abs ` A ) + 1 ) / 2 ) / ( abs ` A ) ) ^ k ) <-> k < ( ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) / ( ( abs ` A ) ^ k ) ) ) )
73 nn0re 
 |-  ( k e. NN0 -> k e. RR )
74 73 adantl 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ k e. NN0 ) -> k e. RR )
75 reexpcl 
 |-  ( ( ( ( ( abs ` A ) + 1 ) / 2 ) e. RR /\ k e. NN0 ) -> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) e. RR )
76 44 75 sylan 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ k e. NN0 ) -> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) e. RR )
77 40 adantr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) -> ( abs ` A ) e. RR )
78 reexpcl 
 |-  ( ( ( abs ` A ) e. RR /\ k e. NN0 ) -> ( ( abs ` A ) ^ k ) e. RR )
79 77 78 sylan 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ k e. NN0 ) -> ( ( abs ` A ) ^ k ) e. RR )
80 77 adantr 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ k e. NN0 ) -> ( abs ` A ) e. RR )
81 nn0z 
 |-  ( k e. NN0 -> k e. ZZ )
82 81 adantl 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ k e. NN0 ) -> k e. ZZ )
83 68 rpgt0d 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ k e. NN0 ) -> 0 < ( abs ` A ) )
84 expgt0 
 |-  ( ( ( abs ` A ) e. RR /\ k e. ZZ /\ 0 < ( abs ` A ) ) -> 0 < ( ( abs ` A ) ^ k ) )
85 80 82 83 84 syl3anc 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ k e. NN0 ) -> 0 < ( ( abs ` A ) ^ k ) )
86 ltmuldiv 
 |-  ( ( k e. RR /\ ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) e. RR /\ ( ( ( abs ` A ) ^ k ) e. RR /\ 0 < ( ( abs ` A ) ^ k ) ) ) -> ( ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) <-> k < ( ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) / ( ( abs ` A ) ^ k ) ) ) )
87 74 76 79 85 86 syl112anc 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ k e. NN0 ) -> ( ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) <-> k < ( ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) / ( ( abs ` A ) ^ k ) ) ) )
88 72 87 bitr4d 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ k e. NN0 ) -> ( ( 1 x. k ) < ( ( ( ( ( abs ` A ) + 1 ) / 2 ) / ( abs ` A ) ) ^ k ) <-> ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) )
89 61 88 sylan2 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ ( n e. NN0 /\ k e. ( ZZ>= ` n ) ) ) -> ( ( 1 x. k ) < ( ( ( ( ( abs ` A ) + 1 ) / 2 ) / ( abs ` A ) ) ^ k ) <-> ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) )
90 89 anassrs 
 |-  ( ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ n e. NN0 ) /\ k e. ( ZZ>= ` n ) ) -> ( ( 1 x. k ) < ( ( ( ( ( abs ` A ) + 1 ) / 2 ) / ( abs ` A ) ) ^ k ) <-> ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) )
91 90 ralbidva 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ n e. NN0 ) -> ( A. k e. ( ZZ>= ` n ) ( 1 x. k ) < ( ( ( ( ( abs ` A ) + 1 ) / 2 ) / ( abs ` A ) ) ^ k ) <-> A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) )
92 simprl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) -> n e. NN0 )
93 oveq2 
 |-  ( k = m -> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) = ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ m ) )
94 eqid 
 |-  ( k e. NN0 |-> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) = ( k e. NN0 |-> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) )
95 ovex 
 |-  ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ m ) e. _V
96 93 94 95 fvmpt 
 |-  ( m e. NN0 -> ( ( k e. NN0 |-> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ` m ) = ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ m ) )
97 96 adantl 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. NN0 ) -> ( ( k e. NN0 |-> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ` m ) = ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ m ) )
98 43 ad2antrr 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. NN0 ) -> ( ( ( abs ` A ) + 1 ) / 2 ) e. RR )
99 simpr 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. NN0 ) -> m e. NN0 )
100 98 99 reexpcld 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. NN0 ) -> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ m ) e. RR )
101 97 100 eqeltrd 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. NN0 ) -> ( ( k e. NN0 |-> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ` m ) e. RR )
102 id 
 |-  ( k = m -> k = m )
103 oveq2 
 |-  ( k = m -> ( A ^ k ) = ( A ^ m ) )
104 102 103 oveq12d 
 |-  ( k = m -> ( k x. ( A ^ k ) ) = ( m x. ( A ^ m ) ) )
105 ovex 
 |-  ( m x. ( A ^ m ) ) e. _V
106 104 1 105 fvmpt 
 |-  ( m e. NN0 -> ( F ` m ) = ( m x. ( A ^ m ) ) )
107 106 adantl 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. NN0 ) -> ( F ` m ) = ( m x. ( A ^ m ) ) )
108 nn0cn 
 |-  ( m e. NN0 -> m e. CC )
109 108 adantl 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. NN0 ) -> m e. CC )
110 expcl 
 |-  ( ( A e. CC /\ m e. NN0 ) -> ( A ^ m ) e. CC )
111 110 ad4ant14 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. NN0 ) -> ( A ^ m ) e. CC )
112 109 111 mulcld 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. NN0 ) -> ( m x. ( A ^ m ) ) e. CC )
113 107 112 eqeltrd 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. NN0 ) -> ( F ` m ) e. CC )
114 0red 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 0 e. RR )
115 absge0 
 |-  ( A e. CC -> 0 <_ ( abs ` A ) )
116 115 adantr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 0 <_ ( abs ` A ) )
117 114 40 43 116 54 lelttrd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 0 < ( ( ( abs ` A ) + 1 ) / 2 ) )
118 114 43 117 ltled 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 0 <_ ( ( ( abs ` A ) + 1 ) / 2 ) )
119 43 118 absidd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` ( ( ( abs ` A ) + 1 ) / 2 ) ) = ( ( ( abs ` A ) + 1 ) / 2 ) )
120 avglt2 
 |-  ( ( ( abs ` A ) e. RR /\ 1 e. RR ) -> ( ( abs ` A ) < 1 <-> ( ( ( abs ` A ) + 1 ) / 2 ) < 1 ) )
121 40 51 120 sylancl 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( abs ` A ) < 1 <-> ( ( ( abs ` A ) + 1 ) / 2 ) < 1 ) )
122 50 121 mpbid 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( ( abs ` A ) + 1 ) / 2 ) < 1 )
123 119 122 eqbrtrd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` ( ( ( abs ` A ) + 1 ) / 2 ) ) < 1 )
124 oveq2 
 |-  ( k = n -> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) = ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ n ) )
125 ovex 
 |-  ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ n ) e. _V
126 124 94 125 fvmpt 
 |-  ( n e. NN0 -> ( ( k e. NN0 |-> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ` n ) = ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ n ) )
127 126 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( ( k e. NN0 |-> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ` n ) = ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ n ) )
128 65 123 127 geolim 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( k e. NN0 |-> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) ~~> ( 1 / ( 1 - ( ( ( abs ` A ) + 1 ) / 2 ) ) ) )
129 seqex 
 |-  seq 0 ( + , ( k e. NN0 |-> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) e. _V
130 ovex 
 |-  ( 1 / ( 1 - ( ( ( abs ` A ) + 1 ) / 2 ) ) ) e. _V
131 129 130 breldm 
 |-  ( seq 0 ( + , ( k e. NN0 |-> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) ~~> ( 1 / ( 1 - ( ( ( abs ` A ) + 1 ) / 2 ) ) ) -> seq 0 ( + , ( k e. NN0 |-> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) e. dom ~~> )
132 128 131 syl 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( k e. NN0 |-> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) e. dom ~~> )
133 132 adantr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) -> seq 0 ( + , ( k e. NN0 |-> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) e. dom ~~> )
134 1red 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) -> 1 e. RR )
135 eluznn0 
 |-  ( ( n e. NN0 /\ m e. ( ZZ>= ` n ) ) -> m e. NN0 )
136 92 135 sylan 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> m e. NN0 )
137 136 nn0red 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> m e. RR )
138 simplll 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> A e. CC )
139 138 abscld 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( abs ` A ) e. RR )
140 139 136 reexpcld 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( ( abs ` A ) ^ m ) e. RR )
141 137 140 remulcld 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( m x. ( ( abs ` A ) ^ m ) ) e. RR )
142 136 100 syldan 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ m ) e. RR )
143 simprr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) -> A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) )
144 oveq2 
 |-  ( k = m -> ( ( abs ` A ) ^ k ) = ( ( abs ` A ) ^ m ) )
145 102 144 oveq12d 
 |-  ( k = m -> ( k x. ( ( abs ` A ) ^ k ) ) = ( m x. ( ( abs ` A ) ^ m ) ) )
146 145 93 breq12d 
 |-  ( k = m -> ( ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) <-> ( m x. ( ( abs ` A ) ^ m ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ m ) ) )
147 146 rspccva 
 |-  ( ( A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) /\ m e. ( ZZ>= ` n ) ) -> ( m x. ( ( abs ` A ) ^ m ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ m ) )
148 143 147 sylan 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( m x. ( ( abs ` A ) ^ m ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ m ) )
149 141 142 148 ltled 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( m x. ( ( abs ` A ) ^ m ) ) <_ ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ m ) )
150 136 nn0cnd 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> m e. CC )
151 138 136 expcld 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( A ^ m ) e. CC )
152 150 151 absmuld 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( abs ` ( m x. ( A ^ m ) ) ) = ( ( abs ` m ) x. ( abs ` ( A ^ m ) ) ) )
153 136 nn0ge0d 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> 0 <_ m )
154 137 153 absidd 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( abs ` m ) = m )
155 138 136 absexpd 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( abs ` ( A ^ m ) ) = ( ( abs ` A ) ^ m ) )
156 154 155 oveq12d 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( ( abs ` m ) x. ( abs ` ( A ^ m ) ) ) = ( m x. ( ( abs ` A ) ^ m ) ) )
157 152 156 eqtrd 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( abs ` ( m x. ( A ^ m ) ) ) = ( m x. ( ( abs ` A ) ^ m ) ) )
158 142 recnd 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ m ) e. CC )
159 158 mulid2d 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( 1 x. ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ m ) ) = ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ m ) )
160 149 157 159 3brtr4d 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( abs ` ( m x. ( A ^ m ) ) ) <_ ( 1 x. ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ m ) ) )
161 136 106 syl 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( F ` m ) = ( m x. ( A ^ m ) ) )
162 161 fveq2d 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( abs ` ( F ` m ) ) = ( abs ` ( m x. ( A ^ m ) ) ) )
163 136 96 syl 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( ( k e. NN0 |-> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ` m ) = ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ m ) )
164 163 oveq2d 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( 1 x. ( ( k e. NN0 |-> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ` m ) ) = ( 1 x. ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ m ) ) )
165 160 162 164 3brtr4d 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) /\ m e. ( ZZ>= ` n ) ) -> ( abs ` ( F ` m ) ) <_ ( 1 x. ( ( k e. NN0 |-> ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ` m ) ) )
166 25 92 101 113 133 134 165 cvgcmpce 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ ( n e. NN0 /\ A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) ) ) -> seq 0 ( + , F ) e. dom ~~> )
167 166 expr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) -> seq 0 ( + , F ) e. dom ~~> ) )
168 167 adantlr 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ n e. NN0 ) -> ( A. k e. ( ZZ>= ` n ) ( k x. ( ( abs ` A ) ^ k ) ) < ( ( ( ( abs ` A ) + 1 ) / 2 ) ^ k ) -> seq 0 ( + , F ) e. dom ~~> ) )
169 91 168 sylbid 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) /\ n e. NN0 ) -> ( A. k e. ( ZZ>= ` n ) ( 1 x. k ) < ( ( ( ( ( abs ` A ) + 1 ) / 2 ) / ( abs ` A ) ) ^ k ) -> seq 0 ( + , F ) e. dom ~~> ) )
170 169 rexlimdva 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) -> ( E. n e. NN0 A. k e. ( ZZ>= ` n ) ( 1 x. k ) < ( ( ( ( ( abs ` A ) + 1 ) / 2 ) / ( abs ` A ) ) ^ k ) -> seq 0 ( + , F ) e. dom ~~> ) )
171 60 170 mpd 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ A =/= 0 ) -> seq 0 ( + , F ) e. dom ~~> )
172 37 171 pm2.61dane 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , F ) e. dom ~~> )