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

Metamath Proof Explorer

Theorem geoisum

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

Ref Expression
Assertion geoisum ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → Σ 𝑘 ∈ ℕ0 ( 𝐴 ↑ 𝑘 ) = ( 1 / ( 1 − 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
2 0zd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 0 ∈ ℤ )
3 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐴 ↑ 𝑛 ) = ( 𝐴 ↑ 𝑘 ) )
4 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) )
5 ovex ⊢ ( 𝐴 ↑ 𝑘 ) ∈ V
6 3 4 5 fvmpt ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
7 6 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
8 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
9 8 adantlr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
10 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 𝐴 ∈ ℂ )
11 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ 𝐴 ) < 1 )
12 10 11 7 geolim ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ) ⇝ ( 1 / ( 1 − 𝐴 ) ) )
13 1 2 7 9 12 isumclim ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → Σ 𝑘 ∈ ℕ0 ( 𝐴 ↑ 𝑘 ) = ( 1 / ( 1 − 𝐴 ) ) )