Metamath Proof Explorer

Theorem geoserg

Description: The value of the finite geometric series A ^ M + A ^ ( M + 1 ) + ... + A ^ ( N - 1 ) . (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses geoserg.1 
|- ( ph -> A e. CC )
geoserg.2 
|- ( ph -> A =/= 1 )
geoserg.3 
|- ( ph -> M e. NN0 )
geoserg.4 
|- ( ph -> N e. ( ZZ>= ` M ) )
Assertion geoserg 
|- ( ph -> sum_ k e. ( M ..^ N ) ( A ^ k ) = ( ( ( A ^ M ) - ( A ^ N ) ) / ( 1 - A ) ) )

Proof

Step Hyp Ref Expression
1 geoserg.1 
 |-  ( ph -> A e. CC )
2 geoserg.2 
 |-  ( ph -> A =/= 1 )
3 geoserg.3 
 |-  ( ph -> M e. NN0 )
4 geoserg.4 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
5 fzofi 
 |-  ( M ..^ N ) e. Fin
6 5 a1i 
 |-  ( ph -> ( M ..^ N ) e. Fin )
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 1 adantr 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> A e. CC )
11 elfzouz 
 |-  ( k e. ( M ..^ N ) -> k e. ( ZZ>= ` M ) )
12 eluznn0 
 |-  ( ( M e. NN0 /\ k e. ( ZZ>= ` M ) ) -> k e. NN0 )
13 3 11 12 syl2an 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> k e. NN0 )
14 10 13 expcld 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( A ^ k ) e. CC )
15 6 9 14 fsummulc1 
 |-  ( ph -> ( sum_ k e. ( M ..^ N ) ( A ^ k ) x. ( 1 - A ) ) = sum_ k e. ( M ..^ N ) ( ( A ^ k ) x. ( 1 - A ) ) )
16 7 a1i 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> 1 e. CC )
17 14 16 10 subdid 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( A ^ k ) x. ( 1 - A ) ) = ( ( ( A ^ k ) x. 1 ) - ( ( A ^ k ) x. A ) ) )
18 14 mulid1d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( A ^ k ) x. 1 ) = ( A ^ k ) )
19 10 13 expp1d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( A ^ ( k + 1 ) ) = ( ( A ^ k ) x. A ) )
20 19 eqcomd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( A ^ k ) x. A ) = ( A ^ ( k + 1 ) ) )
21 18 20 oveq12d 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( ( A ^ k ) x. 1 ) - ( ( A ^ k ) x. A ) ) = ( ( A ^ k ) - ( A ^ ( k + 1 ) ) ) )
22 17 21 eqtrd 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( ( A ^ k ) x. ( 1 - A ) ) = ( ( A ^ k ) - ( A ^ ( k + 1 ) ) ) )
23 22 sumeq2dv 
 |-  ( ph -> sum_ k e. ( M ..^ N ) ( ( A ^ k ) x. ( 1 - A ) ) = sum_ k e. ( M ..^ N ) ( ( A ^ k ) - ( A ^ ( k + 1 ) ) ) )
24 oveq2 
 |-  ( j = k -> ( A ^ j ) = ( A ^ k ) )
25 oveq2 
 |-  ( j = ( k + 1 ) -> ( A ^ j ) = ( A ^ ( k + 1 ) ) )
26 oveq2 
 |-  ( j = M -> ( A ^ j ) = ( A ^ M ) )
27 oveq2 
 |-  ( j = N -> ( A ^ j ) = ( A ^ N ) )
28 1 adantr 
 |-  ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )
29 elfzuz 
 |-  ( j e. ( M ... N ) -> j e. ( ZZ>= ` M ) )
30 eluznn0 
 |-  ( ( M e. NN0 /\ j e. ( ZZ>= ` M ) ) -> j e. NN0 )
31 3 29 30 syl2an 
 |-  ( ( ph /\ j e. ( M ... N ) ) -> j e. NN0 )
32 28 31 expcld 
 |-  ( ( ph /\ j e. ( M ... N ) ) -> ( A ^ j ) e. CC )
33 24 25 26 27 4 32 telfsumo 
 |-  ( ph -> sum_ k e. ( M ..^ N ) ( ( A ^ k ) - ( A ^ ( k + 1 ) ) ) = ( ( A ^ M ) - ( A ^ N ) ) )
34 15 23 33 3eqtrrd 
 |-  ( ph -> ( ( A ^ M ) - ( A ^ N ) ) = ( sum_ k e. ( M ..^ N ) ( A ^ k ) x. ( 1 - A ) ) )
35 1 3 expcld 
 |-  ( ph -> ( A ^ M ) e. CC )
36 eluznn0 
 |-  ( ( M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> N e. NN0 )
37 3 4 36 syl2anc 
 |-  ( ph -> N e. NN0 )
38 1 37 expcld 
 |-  ( ph -> ( A ^ N ) e. CC )
39 35 38 subcld 
 |-  ( ph -> ( ( A ^ M ) - ( A ^ N ) ) e. CC )
40 6 14 fsumcl 
 |-  ( ph -> sum_ k e. ( M ..^ N ) ( A ^ k ) e. CC )
41 2 necomd 
 |-  ( ph -> 1 =/= A )
42 subeq0 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( ( 1 - A ) = 0 <-> 1 = A ) )
43 7 1 42 sylancr 
 |-  ( ph -> ( ( 1 - A ) = 0 <-> 1 = A ) )
44 43 necon3bid 
 |-  ( ph -> ( ( 1 - A ) =/= 0 <-> 1 =/= A ) )
45 41 44 mpbird 
 |-  ( ph -> ( 1 - A ) =/= 0 )
46 39 40 9 45 divmul3d 
 |-  ( ph -> ( ( ( ( A ^ M ) - ( A ^ N ) ) / ( 1 - A ) ) = sum_ k e. ( M ..^ N ) ( A ^ k ) <-> ( ( A ^ M ) - ( A ^ N ) ) = ( sum_ k e. ( M ..^ N ) ( A ^ k ) x. ( 1 - A ) ) ) )
47 34 46 mpbird 
 |-  ( ph -> ( ( ( A ^ M ) - ( A ^ N ) ) / ( 1 - A ) ) = sum_ k e. ( M ..^ N ) ( A ^ k ) )
48 47 eqcomd 
 |-  ( ph -> sum_ k e. ( M ..^ N ) ( A ^ k ) = ( ( ( A ^ M ) - ( A ^ N ) ) / ( 1 - A ) ) )