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

Proof

Step	Hyp	Ref	Expression
1		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
2		0zd	$$⊢\left(A\in ℂ\wedge 1<\left|A\right|\right)\to 0\in \mathbb{Z}$$
3		oveq2	$$⊢n=k\to {\left(\frac{1}{A}\right)}^n={\left(\frac{1}{A}\right)}^k$$
4		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼{\left(\frac{1}{A}\right)}^n\right)=\left(n\in {\mathbb{N}}_0⟼{\left(\frac{1}{A}\right)}^n\right)$$
5		ovex	$$⊢{\left(\frac{1}{A}\right)}^k\in \mathrm{V}$$
6	3 4 5	fvmpt	$$⊢k\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼{\left(\frac{1}{A}\right)}^n\right)\left(k\right)={\left(\frac{1}{A}\right)}^k$$
7	6	adantl	$$⊢\left(\left(A\in ℂ\wedge 1<\left|A\right|\right)\wedge k\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼{\left(\frac{1}{A}\right)}^n\right)\left(k\right)={\left(\frac{1}{A}\right)}^k$$
8		0le1	$$⊢0\le 1$$
9		0re	$$⊢0\in ℝ$$
10		1re	$$⊢1\in ℝ$$
11	9 10	lenlti	$$⊢0\le 1\leftrightarrow \neg 1<0$$
12	8 11	mpbi	$$⊢\neg 1<0$$
13		fveq2	$$⊢A=0\to \left|A\right|=\left|0\right|$$
14		abs0	$$⊢\left|0\right|=0$$
15	13 14	eqtrdi	$$⊢A=0\to \left|A\right|=0$$
16	15	breq2d	$$⊢A=0\to \left(1<\left|A\right|\leftrightarrow 1<0\right)$$
17	12 16	mtbiri	$$⊢A=0\to \neg 1<\left|A\right|$$
18	17	necon2ai	$$⊢1<\left|A\right|\to A\ne 0$$
19		reccl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{1}{A}\in ℂ$$
20	18 19	sylan2	$$⊢\left(A\in ℂ\wedge 1<\left|A\right|\right)\to \frac{1}{A}\in ℂ$$
21		expcl	$$⊢\left(\frac{1}{A}\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to {\left(\frac{1}{A}\right)}^k\in ℂ$$
22	20 21	sylan	$$⊢\left(\left(A\in ℂ\wedge 1<\left|A\right|\right)\wedge k\in {\mathbb{N}}_0\right)\to {\left(\frac{1}{A}\right)}^k\in ℂ$$
23		simpl	$$⊢\left(A\in ℂ\wedge 1<\left|A\right|\right)\to A\in ℂ$$
24		simpr	$$⊢\left(A\in ℂ\wedge 1<\left|A\right|\right)\to 1<\left|A\right|$$
25	23 24 7	georeclim	$$⊢\left(A\in ℂ\wedge 1<\left|A\right|\right)\to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼{\left(\frac{1}{A}\right)}^n\right)\right)⇝\left(\frac{A}{A-1}\right)$$
26	1 2 7 22 25	isumclim	$$⊢\left(A\in ℂ\wedge 1<\left|A\right|\right)\to \sum _{k\in {\mathbb{N}}_0}{\left(\frac{1}{A}\right)}^k=\frac{A}{A-1}$$