Metamath Proof Explorer

Theorem geoisumr

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

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

Proof

Step Hyp Ref Expression
1 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
2 0zd ⊢ A ∈ ℂ ∧ 1 < A → 0 ∈ ℤ
3 oveq2 ⊢ n = k → 1 A n = 1 A k
4 eqid ⊢ n ∈ ℕ 0 ⟼ 1 A n = n ∈ ℕ 0 ⟼ 1 A n
5 ovex ⊢ 1 A k ∈ V
6 3 4 5 fvmpt ⊢ k ∈ ℕ 0 → n ∈ ℕ 0 ⟼ 1 A n ⁡ k = 1 A k
7 6 adantl ⊢ A ∈ ℂ ∧ 1 < A ∧ k ∈ ℕ 0 → n ∈ ℕ 0 ⟼ 1 A n ⁡ k = 1 A k
8 0le1 ⊢ 0 ≤ 1
9 0re ⊢ 0 ∈ ℝ
10 1re ⊢ 1 ∈ ℝ
11 9 10 lenlti ⊢ 0 ≤ 1 ↔ ¬ 1 < 0
12 8 11 mpbi ⊢ ¬ 1 < 0
13 fveq2 ⊢ A = 0 → A = 0
14 abs0 ⊢ 0 = 0
15 13 14 eqtrdi ⊢ A = 0 → A = 0
16 15 breq2d ⊢ A = 0 → 1 < A ↔ 1 < 0
17 12 16 mtbiri ⊢ A = 0 → ¬ 1 < A
18 17 necon2ai ⊢ 1 < A → A ≠ 0
19 reccl ⊢ A ∈ ℂ ∧ A ≠ 0 → 1 A ∈ ℂ
20 18 19 sylan2 ⊢ A ∈ ℂ ∧ 1 < A → 1 A ∈ ℂ
21 expcl ⊢ 1 A ∈ ℂ ∧ k ∈ ℕ 0 → 1 A k ∈ ℂ
22 20 21 sylan ⊢ A ∈ ℂ ∧ 1 < A ∧ k ∈ ℕ 0 → 1 A k ∈ ℂ
23 simpl ⊢ A ∈ ℂ ∧ 1 < A → A ∈ ℂ
24 simpr ⊢ A ∈ ℂ ∧ 1 < A → 1 < A
25 23 24 7 georeclim ⊢ A ∈ ℂ ∧ 1 < A → seq 0 + n ∈ ℕ 0 ⟼ 1 A n ⇝ A A − 1
26 1 2 7 22 25 isumclim ⊢ A ∈ ℂ ∧ 1 < A → ∑ k ∈ ℕ 0 1 A k = A A − 1