Metamath Proof Explorer

Theorem geoisum1

Description: The infinite sum of A ^ 1 + A ^ 2 ... is ( A / ( 1 - A ) ) . (Contributed by NM, 1-Nov-2007) (Revised by Mario Carneiro, 26-Apr-2014)

Ref Expression
Assertion geoisum1 ⊢ A ∈ ℂ ∧ A < 1 → ∑ k ∈ ℕ A k = A 1 − A

Proof

Step Hyp Ref Expression
1 nnuz ⊢ ℕ = ℤ ≥ 1
2 1zzd ⊢ A ∈ ℂ ∧ A < 1 → 1 ∈ ℤ
3 oveq2 ⊢ n = k → A n = A k
4 eqid ⊢ n ∈ ℕ ⟼ A n = n ∈ ℕ ⟼ A n
5 ovex ⊢ A k ∈ V
6 3 4 5 fvmpt ⊢ k ∈ ℕ → n ∈ ℕ ⟼ A n ⁡ k = A k
7 6 adantl ⊢ A ∈ ℂ ∧ A < 1 ∧ k ∈ ℕ → n ∈ ℕ ⟼ A n ⁡ k = A k
8 simpl ⊢ A ∈ ℂ ∧ A < 1 → A ∈ ℂ
9 nnnn0 ⊢ k ∈ ℕ → k ∈ ℕ 0
10 expcl ⊢ A ∈ ℂ ∧ k ∈ ℕ 0 → A k ∈ ℂ
11 8 9 10 syl2an ⊢ A ∈ ℂ ∧ A < 1 ∧ k ∈ ℕ → A k ∈ ℂ
12 simpr ⊢ A ∈ ℂ ∧ A < 1 → A < 1
13 1nn0 ⊢ 1 ∈ ℕ 0
14 13 a1i ⊢ A ∈ ℂ ∧ A < 1 → 1 ∈ ℕ 0
15 elnnuz ⊢ k ∈ ℕ ↔ k ∈ ℤ ≥ 1
16 15 7 sylan2br ⊢ A ∈ ℂ ∧ A < 1 ∧ k ∈ ℤ ≥ 1 → n ∈ ℕ ⟼ A n ⁡ k = A k
17 8 12 14 16 geolim2 ⊢ A ∈ ℂ ∧ A < 1 → seq 1 + n ∈ ℕ ⟼ A n ⇝ A 1 1 − A
18 1 2 7 11 17 isumclim ⊢ A ∈ ℂ ∧ A < 1 → ∑ k ∈ ℕ A k = A 1 1 − A
19 exp1 ⊢ A ∈ ℂ → A 1 = A
20 19 adantr ⊢ A ∈ ℂ ∧ A < 1 → A 1 = A
21 20 oveq1d ⊢ A ∈ ℂ ∧ A < 1 → A 1 1 − A = A 1 − A
22 18 21 eqtrd ⊢ A ∈ ℂ ∧ A < 1 → ∑ k ∈ ℕ A k = A 1 − A