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

Metamath Proof Explorer

Theorem geolim2

Description: The partial sums in the geometric series A ^ M + A ^ ( M + 1 ) ... converge to ( ( A ^ M ) / ( 1 - A ) ) . (Contributed by NM, 6-Jun-2006) (Revised by Mario Carneiro, 26-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 geolim.1 
 |-  ( ph -> A e. CC )
2 geolim.2 
 |-  ( ph -> ( abs ` A ) < 1 )
3 geolim2.3 
 |-  ( ph -> M e. NN0 )
4 geolim2.4 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = ( A ^ k ) )
5 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
6 3 nn0zd 
 |-  ( ph -> M e. ZZ )
7 1 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> A e. CC )
8 eluznn0 
 |-  ( ( M e. NN0 /\ k e. ( ZZ>= ` M ) ) -> k e. NN0 )
9 3 8 sylan 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> k e. NN0 )
10 7 9 expcld 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( A ^ k ) e. CC )
11 oveq2 
 |-  ( n = k -> ( A ^ n ) = ( A ^ k ) )
12 eqid 
 |-  ( n e. NN0 |-> ( A ^ n ) ) = ( n e. NN0 |-> ( A ^ n ) )
13 ovex 
 |-  ( A ^ k ) e. _V
14 11 12 13 fvmpt 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = ( A ^ k ) )
15 9 14 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = ( A ^ k ) )
16 15 4 eqtr4d 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = ( F ` k ) )
17 6 16 seqfeq 
 |-  ( ph -> seq M ( + , ( n e. NN0 |-> ( A ^ n ) ) ) = seq M ( + , F ) )
18 oveq2 
 |-  ( n = j -> ( A ^ n ) = ( A ^ j ) )
19 ovex 
 |-  ( A ^ j ) e. _V
20 18 12 19 fvmpt 
 |-  ( j e. NN0 -> ( ( n e. NN0 |-> ( A ^ n ) ) ` j ) = ( A ^ j ) )
21 20 adantl 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` j ) = ( A ^ j ) )
22 1 2 21 geolim 
 |-  ( ph -> seq 0 ( + , ( n e. NN0 |-> ( A ^ n ) ) ) ~~> ( 1 / ( 1 - A ) ) )
23 seqex 
 |-  seq 0 ( + , ( n e. NN0 |-> ( A ^ n ) ) ) e. _V
24 ovex 
 |-  ( 1 / ( 1 - A ) ) e. _V
25 23 24 breldm 
 |-  ( seq 0 ( + , ( n e. NN0 |-> ( A ^ n ) ) ) ~~> ( 1 / ( 1 - A ) ) -> seq 0 ( + , ( n e. NN0 |-> ( A ^ n ) ) ) e. dom ~~> )
26 22 25 syl 
 |-  ( ph -> seq 0 ( + , ( n e. NN0 |-> ( A ^ n ) ) ) e. dom ~~> )
27 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
28 expcl 
 |-  ( ( A e. CC /\ j e. NN0 ) -> ( A ^ j ) e. CC )
29 1 28 sylan 
 |-  ( ( ph /\ j e. NN0 ) -> ( A ^ j ) e. CC )
30 21 29 eqeltrd 
 |-  ( ( ph /\ j e. NN0 ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` j ) e. CC )
31 27 3 30 iserex 
 |-  ( ph -> ( seq 0 ( + , ( n e. NN0 |-> ( A ^ n ) ) ) e. dom ~~> <-> seq M ( + , ( n e. NN0 |-> ( A ^ n ) ) ) e. dom ~~> ) )
32 26 31 mpbid 
 |-  ( ph -> seq M ( + , ( n e. NN0 |-> ( A ^ n ) ) ) e. dom ~~> )
33 17 32 eqeltrrd 
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )
34 5 6 4 10 33 isumclim2 
 |-  ( ph -> seq M ( + , F ) ~~> sum_ k e. ( ZZ>= ` M ) ( A ^ k ) )
35 14 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( A ^ n ) ) ` k ) = ( A ^ k ) )
36 expcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
37 1 36 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ^ k ) e. CC )
38 27 5 3 35 37 26 isumsplit 
 |-  ( ph -> sum_ k e. NN0 ( A ^ k ) = ( sum_ k e. ( 0 ... ( M - 1 ) ) ( A ^ k ) + sum_ k e. ( ZZ>= ` M ) ( A ^ k ) ) )
39 0zd 
 |-  ( ph -> 0 e. ZZ )
40 27 39 35 37 22 isumclim 
 |-  ( ph -> sum_ k e. NN0 ( A ^ k ) = ( 1 / ( 1 - A ) ) )
41 38 40 eqtr3d 
 |-  ( ph -> ( sum_ k e. ( 0 ... ( M - 1 ) ) ( A ^ k ) + sum_ k e. ( ZZ>= ` M ) ( A ^ k ) ) = ( 1 / ( 1 - A ) ) )
42 1re 
 |-  1 e. RR
43 42 ltnri 
 |-  -. 1 < 1
44 fveq2 
 |-  ( A = 1 -> ( abs ` A ) = ( abs ` 1 ) )
45 abs1 
 |-  ( abs ` 1 ) = 1
46 44 45 eqtrdi 
 |-  ( A = 1 -> ( abs ` A ) = 1 )
47 46 breq1d 
 |-  ( A = 1 -> ( ( abs ` A ) < 1 <-> 1 < 1 ) )
48 43 47 mtbiri 
 |-  ( A = 1 -> -. ( abs ` A ) < 1 )
49 48 necon2ai 
 |-  ( ( abs ` A ) < 1 -> A =/= 1 )
50 2 49 syl 
 |-  ( ph -> A =/= 1 )
51 1 50 3 geoser 
 |-  ( ph -> sum_ k e. ( 0 ... ( M - 1 ) ) ( A ^ k ) = ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) )
52 51 oveq1d 
 |-  ( ph -> ( sum_ k e. ( 0 ... ( M - 1 ) ) ( A ^ k ) + sum_ k e. ( ZZ>= ` M ) ( A ^ k ) ) = ( ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) + sum_ k e. ( ZZ>= ` M ) ( A ^ k ) ) )
53 41 52 eqtr3d 
 |-  ( ph -> ( 1 / ( 1 - A ) ) = ( ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) + sum_ k e. ( ZZ>= ` M ) ( A ^ k ) ) )
54 53 oveq1d 
 |-  ( ph -> ( ( 1 / ( 1 - A ) ) - ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) ) = ( ( ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) + sum_ k e. ( ZZ>= ` M ) ( A ^ k ) ) - ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) ) )
55 1cnd 
 |-  ( ph -> 1 e. CC )
56 ax-1cn 
 |-  1 e. CC
57 1 3 expcld 
 |-  ( ph -> ( A ^ M ) e. CC )
58 subcl 
 |-  ( ( 1 e. CC /\ ( A ^ M ) e. CC ) -> ( 1 - ( A ^ M ) ) e. CC )
59 56 57 58 sylancr 
 |-  ( ph -> ( 1 - ( A ^ M ) ) e. CC )
60 subcl 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( 1 - A ) e. CC )
61 56 1 60 sylancr 
 |-  ( ph -> ( 1 - A ) e. CC )
62 50 necomd 
 |-  ( ph -> 1 =/= A )
63 subeq0 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( ( 1 - A ) = 0 <-> 1 = A ) )
64 56 1 63 sylancr 
 |-  ( ph -> ( ( 1 - A ) = 0 <-> 1 = A ) )
65 64 necon3bid 
 |-  ( ph -> ( ( 1 - A ) =/= 0 <-> 1 =/= A ) )
66 62 65 mpbird 
 |-  ( ph -> ( 1 - A ) =/= 0 )
67 55 59 61 66 divsubdird 
 |-  ( ph -> ( ( 1 - ( 1 - ( A ^ M ) ) ) / ( 1 - A ) ) = ( ( 1 / ( 1 - A ) ) - ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) ) )
68 nncan 
 |-  ( ( 1 e. CC /\ ( A ^ M ) e. CC ) -> ( 1 - ( 1 - ( A ^ M ) ) ) = ( A ^ M ) )
69 56 57 68 sylancr 
 |-  ( ph -> ( 1 - ( 1 - ( A ^ M ) ) ) = ( A ^ M ) )
70 69 oveq1d 
 |-  ( ph -> ( ( 1 - ( 1 - ( A ^ M ) ) ) / ( 1 - A ) ) = ( ( A ^ M ) / ( 1 - A ) ) )
71 67 70 eqtr3d 
 |-  ( ph -> ( ( 1 / ( 1 - A ) ) - ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) ) = ( ( A ^ M ) / ( 1 - A ) ) )
72 59 61 66 divcld 
 |-  ( ph -> ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) e. CC )
73 5 6 15 10 32 isumcl 
 |-  ( ph -> sum_ k e. ( ZZ>= ` M ) ( A ^ k ) e. CC )
74 72 73 pncan2d 
 |-  ( ph -> ( ( ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) + sum_ k e. ( ZZ>= ` M ) ( A ^ k ) ) - ( ( 1 - ( A ^ M ) ) / ( 1 - A ) ) ) = sum_ k e. ( ZZ>= ` M ) ( A ^ k ) )
75 54 71 74 3eqtr3rd 
 |-  ( ph -> sum_ k e. ( ZZ>= ` M ) ( A ^ k ) = ( ( A ^ M ) / ( 1 - A ) ) )
76 34 75 breqtrd 
 |-  ( ph -> seq M ( + , F ) ~~> ( ( A ^ M ) / ( 1 - A ) ) )