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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	geoser.2	⊢ ( 𝜑 → 𝐴 ≠ 1 )
	geoser.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	geoser	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 ↑ 𝑘 ) = ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) / ( 1 − 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		geoser.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		geoser.2	⊢ ( 𝜑 → 𝐴 ≠ 1 )
3		geoser.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4		0nn0	⊢ 0 ∈ ℕ0
5	4	a1i	⊢ ( 𝜑 → 0 ∈ ℕ0 )
6		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
7	3 6	eleqtrdi	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
8	1 2 5 7	geoserg	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝐴 ↑ 𝑘 ) = ( ( ( 𝐴 ↑ 0 ) − ( 𝐴 ↑ 𝑁 ) ) / ( 1 − 𝐴 ) ) )
9	3	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
10		fzoval	⊢ ( 𝑁 ∈ ℤ → ( 0 ..^ 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
11	9 10	syl	⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) = ( 0 ... ( 𝑁 − 1 ) ) )
12	11	sumeq1d	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( 𝐴 ↑ 𝑘 ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 ↑ 𝑘 ) )
13	1	exp0d	⊢ ( 𝜑 → ( 𝐴 ↑ 0 ) = 1 )
14	13	oveq1d	⊢ ( 𝜑 → ( ( 𝐴 ↑ 0 ) − ( 𝐴 ↑ 𝑁 ) ) = ( 1 − ( 𝐴 ↑ 𝑁 ) ) )
15	14	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 0 ) − ( 𝐴 ↑ 𝑁 ) ) / ( 1 − 𝐴 ) ) = ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) / ( 1 − 𝐴 ) ) )
16	8 12 15	3eqtr3d	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 ↑ 𝑘 ) = ( ( 1 − ( 𝐴 ↑ 𝑁 ) ) / ( 1 − 𝐴 ) ) )