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 ) ) )