Metamath Proof Explorer

Theorem geolim

Description: The partial sums in the infinite series 1 + A ^ 1 + A ^ 2 ... converge to ( 1 / ( 1 - A ) ) . (Contributed by NM, 15-May-2006)

Ref Expression
Hypotheses geolim.1 
|- ( ph -> A e. CC )
geolim.2 
|- ( ph -> ( abs ` A ) < 1 )
geolim.3 
|- ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( A ^ k ) )
Assertion geolim 
|- ( ph -> seq 0 ( + , F ) ~~> ( 1 / ( 1 - A ) ) )

Proof

Step Hyp Ref Expression
1 geolim.1 
 |-  ( ph -> A e. CC )
2 geolim.2 
 |-  ( ph -> ( abs ` A ) < 1 )
3 geolim.3 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( A ^ k ) )
4 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
5 0zd 
 |-  ( ph -> 0 e. ZZ )
6 1 2 expcnv 
 |-  ( ph -> ( n e. NN0 |-> ( A ^ n ) ) ~~> 0 )
7 ax-1cn 
 |-  1 e. CC
8 subcl 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( 1 - A ) e. CC )
9 7 1 8 sylancr 
 |-  ( ph -> ( 1 - A ) e. CC )
10 1re 
 |-  1 e. RR
11 10 ltnri 
 |-  -. 1 < 1
12 fveq2 
 |-  ( A = 1 -> ( abs ` A ) = ( abs ` 1 ) )
13 abs1 
 |-  ( abs ` 1 ) = 1
14 12 13 eqtrdi 
 |-  ( A = 1 -> ( abs ` A ) = 1 )
15 14 breq1d 
 |-  ( A = 1 -> ( ( abs ` A ) < 1 <-> 1 < 1 ) )
16 11 15 mtbiri 
 |-  ( A = 1 -> -. ( abs ` A ) < 1 )
17 16 necon2ai 
 |-  ( ( abs ` A ) < 1 -> A =/= 1 )
18 2 17 syl 
 |-  ( ph -> A =/= 1 )
19 18 necomd 
 |-  ( ph -> 1 =/= A )
20 subeq0 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( ( 1 - A ) = 0 <-> 1 = A ) )
21 7 1 20 sylancr 
 |-  ( ph -> ( ( 1 - A ) = 0 <-> 1 = A ) )
22 21 necon3bid 
 |-  ( ph -> ( ( 1 - A ) =/= 0 <-> 1 =/= A ) )
23 19 22 mpbird 
 |-  ( ph -> ( 1 - A ) =/= 0 )
24 1 9 23 divcld 
 |-  ( ph -> ( A / ( 1 - A ) ) e. CC )
25 nn0ex 
 |-  NN0 e. _V
26 25 mptex 
 |-  ( n e. NN0 |-> ( ( A ^ ( n + 1 ) ) / ( 1 - A ) ) ) e. _V
27 26 a1i 
 |-  ( ph -> ( n e. NN0 |-> ( ( A ^ ( n + 1 ) ) / ( 1 - A ) ) ) e. _V )
28 oveq2 
 |-  ( n = j -> ( A ^ n ) = ( A ^ j ) )
29 eqid 
 |-  ( n e. NN0 |-> ( A ^ n ) ) = ( n e. NN0 |-> ( A ^ n ) )
30 ovex 
 |-  ( A ^ j ) e. _V
31 28 29 30 fvmpt 
 |-  ( j e. NN0 -> ( ( n e. NN0 |-> ( A ^ n ) ) ` j ) = ( A ^ j ) )
32 31 adantl 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` j ) = ( A ^ j ) )
33 expcl 
 |-  ( ( A e. CC /\ j e. NN0 ) -> ( A ^ j ) e. CC )
34 1 33 sylan 
 |-  ( ( ph /\ j e. NN0 ) -> ( A ^ j ) e. CC )
35 32 34 eqeltrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` j ) e. CC )
36 expp1 
 |-  ( ( A e. CC /\ j e. NN0 ) -> ( A ^ ( j + 1 ) ) = ( ( A ^ j ) x. A ) )
37 1 36 sylan 
 |-  ( ( ph /\ j e. NN0 ) -> ( A ^ ( j + 1 ) ) = ( ( A ^ j ) x. A ) )
38 1 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> A e. CC )
39 34 38 mulcomd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( A ^ j ) x. A ) = ( A x. ( A ^ j ) ) )
40 37 39 eqtrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( A ^ ( j + 1 ) ) = ( A x. ( A ^ j ) ) )
41 40 oveq1d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( A ^ ( j + 1 ) ) / ( 1 - A ) ) = ( ( A x. ( A ^ j ) ) / ( 1 - A ) ) )
42 9 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> ( 1 - A ) e. CC )
43 23 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> ( 1 - A ) =/= 0 )
44 38 34 42 43 div23d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( A x. ( A ^ j ) ) / ( 1 - A ) ) = ( ( A / ( 1 - A ) ) x. ( A ^ j ) ) )
45 41 44 eqtrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( A ^ ( j + 1 ) ) / ( 1 - A ) ) = ( ( A / ( 1 - A ) ) x. ( A ^ j ) ) )
46 oveq1 
 |-  ( n = j -> ( n + 1 ) = ( j + 1 ) )
47 46 oveq2d 
 |-  ( n = j -> ( A ^ ( n + 1 ) ) = ( A ^ ( j + 1 ) ) )
48 47 oveq1d 
 |-  ( n = j -> ( ( A ^ ( n + 1 ) ) / ( 1 - A ) ) = ( ( A ^ ( j + 1 ) ) / ( 1 - A ) ) )
49 eqid 
 |-  ( n e. NN0 |-> ( ( A ^ ( n + 1 ) ) / ( 1 - A ) ) ) = ( n e. NN0 |-> ( ( A ^ ( n + 1 ) ) / ( 1 - A ) ) )
50 ovex 
 |-  ( ( A ^ ( j + 1 ) ) / ( 1 - A ) ) e. _V
51 48 49 50 fvmpt 
 |-  ( j e. NN0 -> ( ( n e. NN0 |-> ( ( A ^ ( n + 1 ) ) / ( 1 - A ) ) ) ` j ) = ( ( A ^ ( j + 1 ) ) / ( 1 - A ) ) )
52 51 adantl 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( n e. NN0 |-> ( ( A ^ ( n + 1 ) ) / ( 1 - A ) ) ) ` j ) = ( ( A ^ ( j + 1 ) ) / ( 1 - A ) ) )
53 32 oveq2d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( A / ( 1 - A ) ) x. ( ( n e. NN0 |-> ( A ^ n ) ) ` j ) ) = ( ( A / ( 1 - A ) ) x. ( A ^ j ) ) )
54 45 52 53 3eqtr4d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( n e. NN0 |-> ( ( A ^ ( n + 1 ) ) / ( 1 - A ) ) ) ` j ) = ( ( A / ( 1 - A ) ) x. ( ( n e. NN0 |-> ( A ^ n ) ) ` j ) ) )
55 4 5 6 24 27 35 54 climmulc2 
 |-  ( ph -> ( n e. NN0 |-> ( ( A ^ ( n + 1 ) ) / ( 1 - A ) ) ) ~~> ( ( A / ( 1 - A ) ) x. 0 ) )
56 24 mul01d 
 |-  ( ph -> ( ( A / ( 1 - A ) ) x. 0 ) = 0 )
57 55 56 breqtrd 
 |-  ( ph -> ( n e. NN0 |-> ( ( A ^ ( n + 1 ) ) / ( 1 - A ) ) ) ~~> 0 )
58 9 23 reccld 
 |-  ( ph -> ( 1 / ( 1 - A ) ) e. CC )
59 seqex 
 |-  seq 0 ( + , F ) e. _V
60 59 a1i 
 |-  ( ph -> seq 0 ( + , F ) e. _V )
61 peano2nn0 
 |-  ( j e. NN0 -> ( j + 1 ) e. NN0 )
62 expcl 
 |-  ( ( A e. CC /\ ( j + 1 ) e. NN0 ) -> ( A ^ ( j + 1 ) ) e. CC )
63 1 61 62 syl2an 
 |-  ( ( ph /\ j e. NN0 ) -> ( A ^ ( j + 1 ) ) e. CC )
64 63 42 43 divcld 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( A ^ ( j + 1 ) ) / ( 1 - A ) ) e. CC )
65 52 64 eqeltrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( n e. NN0 |-> ( ( A ^ ( n + 1 ) ) / ( 1 - A ) ) ) ` j ) e. CC )
66 nn0cn 
 |-  ( j e. NN0 -> j e. CC )
67 66 adantl 
 |-  ( ( ph /\ j e. NN0 ) -> j e. CC )
68 pncan 
 |-  ( ( j e. CC /\ 1 e. CC ) -> ( ( j + 1 ) - 1 ) = j )
69 67 7 68 sylancl 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( j + 1 ) - 1 ) = j )
70 69 oveq2d 
 |-  ( ( ph /\ j e. NN0 ) -> ( 0 ... ( ( j + 1 ) - 1 ) ) = ( 0 ... j ) )
71 70 sumeq1d 
 |-  ( ( ph /\ j e. NN0 ) -> sum_ k e. ( 0 ... ( ( j + 1 ) - 1 ) ) ( A ^ k ) = sum_ k e. ( 0 ... j ) ( A ^ k ) )
72 7 a1i 
 |-  ( ( ph /\ j e. NN0 ) -> 1 e. CC )
73 72 63 42 43 divsubdird 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 1 - ( A ^ ( j + 1 ) ) ) / ( 1 - A ) ) = ( ( 1 / ( 1 - A ) ) - ( ( A ^ ( j + 1 ) ) / ( 1 - A ) ) ) )
74 18 adantr 
 |-  ( ( ph /\ j e. NN0 ) -> A =/= 1 )
75 61 adantl 
 |-  ( ( ph /\ j e. NN0 ) -> ( j + 1 ) e. NN0 )
76 38 74 75 geoser 
 |-  ( ( ph /\ j e. NN0 ) -> sum_ k e. ( 0 ... ( ( j + 1 ) - 1 ) ) ( A ^ k ) = ( ( 1 - ( A ^ ( j + 1 ) ) ) / ( 1 - A ) ) )
77 52 oveq2d 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( 1 / ( 1 - A ) ) - ( ( n e. NN0 |-> ( ( A ^ ( n + 1 ) ) / ( 1 - A ) ) ) ` j ) ) = ( ( 1 / ( 1 - A ) ) - ( ( A ^ ( j + 1 ) ) / ( 1 - A ) ) ) )
78 73 76 77 3eqtr4d 
 |-  ( ( ph /\ j e. NN0 ) -> sum_ k e. ( 0 ... ( ( j + 1 ) - 1 ) ) ( A ^ k ) = ( ( 1 / ( 1 - A ) ) - ( ( n e. NN0 |-> ( ( A ^ ( n + 1 ) ) / ( 1 - A ) ) ) ` j ) ) )
79 simpll 
 |-  ( ( ( ph /\ j e. NN0 ) /\ k e. ( 0 ... j ) ) -> ph )
80 elfznn0 
 |-  ( k e. ( 0 ... j ) -> k e. NN0 )
81 80 adantl 
 |-  ( ( ( ph /\ j e. NN0 ) /\ k e. ( 0 ... j ) ) -> k e. NN0 )
82 79 81 3 syl2anc 
 |-  ( ( ( ph /\ j e. NN0 ) /\ k e. ( 0 ... j ) ) -> ( F ` k ) = ( A ^ k ) )
83 simpr 
 |-  ( ( ph /\ j e. NN0 ) -> j e. NN0 )
84 83 4 eleqtrdi 
 |-  ( ( ph /\ j e. NN0 ) -> j e. ( ZZ>= ` 0 ) )
85 79 1 syl 
 |-  ( ( ( ph /\ j e. NN0 ) /\ k e. ( 0 ... j ) ) -> A e. CC )
86 85 81 expcld 
 |-  ( ( ( ph /\ j e. NN0 ) /\ k e. ( 0 ... j ) ) -> ( A ^ k ) e. CC )
87 82 84 86 fsumser 
 |-  ( ( ph /\ j e. NN0 ) -> sum_ k e. ( 0 ... j ) ( A ^ k ) = ( seq 0 ( + , F ) ` j ) )
88 71 78 87 3eqtr3rd 
 |-  ( ( ph /\ j e. NN0 ) -> ( seq 0 ( + , F ) ` j ) = ( ( 1 / ( 1 - A ) ) - ( ( n e. NN0 |-> ( ( A ^ ( n + 1 ) ) / ( 1 - A ) ) ) ` j ) ) )
89 4 5 57 58 60 65 88 climsubc2 
 |-  ( ph -> seq 0 ( + , F ) ~~> ( ( 1 / ( 1 - A ) ) - 0 ) )
90 58 subid1d 
 |-  ( ph -> ( ( 1 / ( 1 - A ) ) - 0 ) = ( 1 / ( 1 - A ) ) )
91 89 90 breqtrd 
 |-  ( ph -> seq 0 ( + , F ) ~~> ( 1 / ( 1 - A ) ) )