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

### Proof

Step Hyp Ref Expression
1 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
2 0zd ${⊢}\left({A}\in ℂ\wedge \left|{A}\right|<1\right)\to 0\in ℤ$
3 oveq2 ${⊢}{n}={k}\to {{A}}^{{n}}={{A}}^{{k}}$
4 eqid ${⊢}\left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)=\left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)$
5 ovex ${⊢}{{A}}^{{k}}\in \mathrm{V}$
6 3 4 5 fvmpt ${⊢}{k}\in {ℕ}_{0}\to \left({n}\in {ℕ}_{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 {ℕ}_{0}\right)\to \left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)\left({k}\right)={{A}}^{{k}}$
8 expcl ${⊢}\left({A}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {{A}}^{{k}}\in ℂ$
9 8 adantlr ${⊢}\left(\left({A}\in ℂ\wedge \left|{A}\right|<1\right)\wedge {k}\in {ℕ}_{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 {ℕ}_{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 {ℕ}_{0}}{{A}}^{{k}}=\frac{1}{1-{A}}$