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	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to \sum _{k\in {\mathbb{N}}_0}{A}^k=\frac{1}{1-A}$$

Proof

Step	Hyp	Ref	Expression
1		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
2		0zd	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to 0\in \mathbb{Z}$$
3		oveq2	$$⊢n=k\to A^n=A^k$$
4		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼A^n\right)=\left(n\in {\mathbb{N}}_0⟼A^n\right)$$
5		ovex	$$⊢A^k\in \mathrm{V}$$
6	3 4 5	fvmpt	$$⊢k\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼A^n\right)\left(k\right)=A^k$$
7	6	adantl	$$⊢\left(\left(A\in ℂ\wedge \left|A\right|<1\right)\wedge k\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼A^n\right)\left(k\right)=A^k$$
8		expcl	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to A^k\in ℂ$$
9	8	adantlr	$$⊢\left(\left(A\in ℂ\wedge \left|A\right|<1\right)\wedge k\in {\mathbb{N}}_0\right)\to A^k\in ℂ$$
10		simpl	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to A\in ℂ$$
11		simpr	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to \left|A\right|<1$$
12	10 11 7	geolim	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼A^n\right)\right)⇝\left(\frac{1}{1-A}\right)$$
13	1 2 7 9 12	isumclim	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to \sum _{k\in {\mathbb{N}}_0}{A}^k=\frac{1}{1-A}$$