This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℂ ∧ 1 < ( abs ‘ 𝐴 ) ) → Σ 𝑘 ∈ ℕ0 ( ( 1 / 𝐴 ) ↑ 𝑘 ) = ( 𝐴 / ( 𝐴 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
2 0zd ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 < ( abs ‘ 𝐴 ) ) → 0 ∈ ℤ )
3 oveq2 ⊢ ( 𝑛 = 𝑘 → ( ( 1 / 𝐴 ) ↑ 𝑛 ) = ( ( 1 / 𝐴 ) ↑ 𝑘 ) )
4 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / 𝐴 ) ↑ 𝑛 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / 𝐴 ) ↑ 𝑛 ) )
5 ovex ⊢ ( ( 1 / 𝐴 ) ↑ 𝑘 ) ∈ V
6 3 4 5 fvmpt ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) = ( ( 1 / 𝐴 ) ↑ 𝑘 ) )
7 6 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 1 < ( abs ‘ 𝐴 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) = ( ( 1 / 𝐴 ) ↑ 𝑘 ) )
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 ⊢ ( 𝐴 = 0 → ( abs ‘ 𝐴 ) = ( abs ‘ 0 ) )
14 abs0 ⊢ ( abs ‘ 0 ) = 0
15 13 14 eqtrdi ⊢ ( 𝐴 = 0 → ( abs ‘ 𝐴 ) = 0 )
16 15 breq2d ⊢ ( 𝐴 = 0 → ( 1 < ( abs ‘ 𝐴 ) ↔ 1 < 0 ) )
17 12 16 mtbiri ⊢ ( 𝐴 = 0 → ¬ 1 < ( abs ‘ 𝐴 ) )
18 17 necon2ai ⊢ ( 1 < ( abs ‘ 𝐴 ) → 𝐴 ≠ 0 )
19 reccl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℂ )
20 18 19 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 < ( abs ‘ 𝐴 ) ) → ( 1 / 𝐴 ) ∈ ℂ )
21 expcl ⊢ ( ( ( 1 / 𝐴 ) ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 / 𝐴 ) ↑ 𝑘 ) ∈ ℂ )
22 20 21 sylan ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 1 < ( abs ‘ 𝐴 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 / 𝐴 ) ↑ 𝑘 ) ∈ ℂ )
23 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 < ( abs ‘ 𝐴 ) ) → 𝐴 ∈ ℂ )
24 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 < ( abs ‘ 𝐴 ) ) → 1 < ( abs ‘ 𝐴 ) )
25 23 24 7 georeclim ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 < ( abs ‘ 𝐴 ) ) → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 1 / 𝐴 ) ↑ 𝑛 ) ) ) ⇝ ( 𝐴 / ( 𝐴 − 1 ) ) )
26 1 2 7 22 25 isumclim ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 < ( abs ‘ 𝐴 ) ) → Σ 𝑘 ∈ ℕ0 ( ( 1 / 𝐴 ) ↑ 𝑘 ) = ( 𝐴 / ( 𝐴 − 1 ) ) )