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

Metamath Proof Explorer

Theorem geoser

Description: The value of the finite geometric series 1 + A ^ 1 + A ^ 2 + ... + A ^ ( N - 1 ) . This is Metamath 100 proof #66. (Contributed by NM, 12-May-2006) (Proof shortened by Mario Carneiro, 15-Jun-2014)

Ref Expression
Hypotheses geoser.1 
|- ( ph -> A e. CC )
geoser.2 
|- ( ph -> A =/= 1 )
geoser.3 
|- ( ph -> N e. NN0 )
Assertion geoser 
|- ( ph -> sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) = ( ( 1 - ( A ^ N ) ) / ( 1 - A ) ) )

Proof

Step Hyp Ref Expression
1 geoser.1 
 |-  ( ph -> A e. CC )
2 geoser.2 
 |-  ( ph -> A =/= 1 )
3 geoser.3 
 |-  ( ph -> N e. NN0 )
4 0nn0 
 |-  0 e. NN0
5 4 a1i 
 |-  ( ph -> 0 e. NN0 )
6 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
7 3 6 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
8 1 2 5 7 geoserg 
 |-  ( ph -> sum_ k e. ( 0 ..^ N ) ( A ^ k ) = ( ( ( A ^ 0 ) - ( A ^ N ) ) / ( 1 - A ) ) )
9 3 nn0zd 
 |-  ( ph -> N e. ZZ )
10 fzoval 
 |-  ( N e. ZZ -> ( 0 ..^ N ) = ( 0 ... ( N - 1 ) ) )
11 9 10 syl 
 |-  ( ph -> ( 0 ..^ N ) = ( 0 ... ( N - 1 ) ) )
12 11 sumeq1d 
 |-  ( ph -> sum_ k e. ( 0 ..^ N ) ( A ^ k ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) )
13 1 exp0d 
 |-  ( ph -> ( A ^ 0 ) = 1 )
14 13 oveq1d 
 |-  ( ph -> ( ( A ^ 0 ) - ( A ^ N ) ) = ( 1 - ( A ^ N ) ) )
15 14 oveq1d 
 |-  ( ph -> ( ( ( A ^ 0 ) - ( A ^ N ) ) / ( 1 - A ) ) = ( ( 1 - ( A ^ N ) ) / ( 1 - A ) ) )
16 8 12 15 3eqtr3d 
 |-  ( ph -> sum_ k e. ( 0 ... ( N - 1 ) ) ( A ^ k ) = ( ( 1 - ( A ^ N ) ) / ( 1 - A ) ) )