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 − 𝐴 ) ) )