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