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

Proof

Step Hyp Ref Expression
1 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
2 1zzd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 1 ∈ ℤ )
3 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐴 ↑ 𝑛 ) = ( 𝐴 ↑ 𝑘 ) )
4 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( 𝐴 ↑ 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝐴 ↑ 𝑛 ) )
5 ovex ⊢ ( 𝐴 ↑ 𝑘 ) ∈ V
6 3 4 5 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
7 6 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
8 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 𝐴 ∈ ℂ )
9 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
10 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
11 8 9 10 syl2an ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
12 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ 𝐴 ) < 1 )
13 1nn0 ⊢ 1 ∈ ℕ0
14 13 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 1 ∈ ℕ0 )
15 elnnuz ⊢ ( 𝑘 ∈ ℕ ↔ 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
16 15 7 sylan2br ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
17 8 12 14 16 geolim2 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝐴 ↑ 𝑛 ) ) ) ⇝ ( ( 𝐴 ↑ 1 ) / ( 1 − 𝐴 ) ) )
18 1 2 7 11 17 isumclim ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → Σ 𝑘 ∈ ℕ ( 𝐴 ↑ 𝑘 ) = ( ( 𝐴 ↑ 1 ) / ( 1 − 𝐴 ) ) )
19 exp1 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 1 ) = 𝐴 )
20 19 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 𝐴 ↑ 1 ) = 𝐴 )
21 20 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( ( 𝐴 ↑ 1 ) / ( 1 − 𝐴 ) ) = ( 𝐴 / ( 1 − 𝐴 ) ) )
22 18 21 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → Σ 𝑘 ∈ ℕ ( 𝐴 ↑ 𝑘 ) = ( 𝐴 / ( 1 − 𝐴 ) ) )