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 ⊢ φ → A ∈ ℂ
geoser.2 ⊢ φ → A ≠ 1
geoser.3 ⊢ φ → N ∈ ℕ 0
Assertion geoser ⊢ φ → ∑ k = 0 N − 1 A k = 1 − A N 1 − A

Proof

Step Hyp Ref Expression
1 geoser.1 ⊢ φ → A ∈ ℂ
2 geoser.2 ⊢ φ → A ≠ 1
3 geoser.3 ⊢ φ → N ∈ ℕ 0
4 0nn0 ⊢ 0 ∈ ℕ 0
5 4 a1i ⊢ φ → 0 ∈ ℕ 0
6 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
7 3 6 eleqtrdi ⊢ φ → N ∈ ℤ ≥ 0
8 1 2 5 7 geoserg ⊢ φ → ∑ k ∈ 0 ..^ N A k = A 0 − A N 1 − A
9 3 nn0zd ⊢ φ → N ∈ ℤ
10 fzoval ⊢ N ∈ ℤ → 0 ..^ N = 0 … N − 1
11 9 10 syl ⊢ φ → 0 ..^ N = 0 … N − 1
12 11 sumeq1d ⊢ φ → ∑ k ∈ 0 ..^ N A k = ∑ k = 0 N − 1 A k
13 1 exp0d ⊢ φ → A 0 = 1
14 13 oveq1d ⊢ φ → A 0 − A N = 1 − A N
15 14 oveq1d ⊢ φ → A 0 − A N 1 − A = 1 − A N 1 − A
16 8 12 15 3eqtr3d ⊢ φ → ∑ k = 0 N − 1 A k = 1 − A N 1 − A