This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ (A \in ℂ \land \|A\| < 1) \to \sum_{k \in ℕ_{0}} A^{k} = \frac{1}{1 - A}$

Proof

Step	Hyp	Ref	Expression
1		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
2		0zd	$⊢ (A \in ℂ \land \|A\| < 1) \to 0 \in ℤ$
3		oveq2	$⊢ n = k \to A^{n} = A^{k}$
4		eqid	$⊢ (n \in ℕ_{0} ⟼ A^{n}) = (n \in ℕ_{0} ⟼ A^{n})$
5		ovex	$⊢ A^{k} \in V$
6	3 4 5	fvmpt	$⊢ k \in ℕ_{0} \to (n \in ℕ_{0} ⟼ A^{n}) (k) = A^{k}$
7	6	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ_{0}) \to (n \in ℕ_{0} ⟼ A^{n}) (k) = A^{k}$
8		expcl	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to A^{k} \in ℂ$
9	8	adantlr	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ_{0}) \to A^{k} \in ℂ$
10		simpl	$⊢ (A \in ℂ \land \|A\| < 1) \to A \in ℂ$
11		simpr	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A\| < 1$
12	10 11 7	geolim	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 0 (+ (n \in ℕ_{0} ⟼ A^{n})) ⇝ (\frac{1}{1 - A})$
13	1 2 7 9 12	isumclim	$⊢ (A \in ℂ \land \|A\| < 1) \to \sum_{k \in ℕ_{0}} A^{k} = \frac{1}{1 - A}$