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 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
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 − 𝐴 ) ) )