geoisum1

Description: The infinite sum of A ^ 1 + A ^ 2 ... is ( A / ( 1 - A ) ) . (Contributed by NM, 1-Nov-2007) (Revised by Mario Carneiro, 26-Apr-2014)

		Ref	Expression
	Assertion	geoisum1	$⊢ (A \in ℂ \land \|A\| < 1) \to \sum_{k \in ℕ} A^{k} = \frac{A}{1 - A}$

Proof

Step	Hyp	Ref	Expression
1		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
2		1zzd	$⊢ (A \in ℂ \land \|A\| < 1) \to 1 \in ℤ$
3		oveq2	$⊢ n = k \to A^{n} = A^{k}$
4		eqid	$⊢ (n \in ℕ ⟼ A^{n}) = (n \in ℕ ⟼ A^{n})$
5		ovex	$⊢ A^{k} \in V$
6	3 4 5	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ A^{n}) (k) = A^{k}$
7	6	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to (n \in ℕ ⟼ A^{n}) (k) = A^{k}$
8		simpl	$⊢ (A \in ℂ \land \|A\| < 1) \to A \in ℂ$
9		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
10		expcl	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to A^{k} \in ℂ$
11	8 9 10	syl2an	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to A^{k} \in ℂ$
12		simpr	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A\| < 1$
13		1nn0	$⊢ 1 \in ℕ_{0}$
14	13	a1i	$⊢ (A \in ℂ \land \|A\| < 1) \to 1 \in ℕ_{0}$
15		elnnuz	$⊢ k \in ℕ \leftrightarrow k \in ℤ_{\geq 1}$
16	15 7	sylan2br	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℤ_{\geq 1}) \to (n \in ℕ ⟼ A^{n}) (k) = A^{k}$
17	8 12 14 16	geolim2	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 1 (+ (n \in ℕ ⟼ A^{n})) ⇝ (\frac{A^{1}}{1 - A})$
18	1 2 7 11 17	isumclim	$⊢ (A \in ℂ \land \|A\| < 1) \to \sum_{k \in ℕ} A^{k} = \frac{A^{1}}{1 - A}$
19		exp1	$⊢ A \in ℂ \to A^{1} = A$
20	19	adantr	$⊢ (A \in ℂ \land \|A\| < 1) \to A^{1} = A$
21	20	oveq1d	$⊢ (A \in ℂ \land \|A\| < 1) \to \frac{A^{1}}{1 - A} = \frac{A}{1 - A}$
22	18 21	eqtrd	$⊢ (A \in ℂ \land \|A\| < 1) \to \sum_{k \in ℕ} A^{k} = \frac{A}{1 - A}$

Metamath Proof Explorer

Theorem geoisum1

Proof