geoisum1c

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

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

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℂ \land R \in ℂ \land \|R\| < 1) \to A \in ℂ$
2		simp2	$⊢ (A \in ℂ \land R \in ℂ \land \|R\| < 1) \to R \in ℂ$
3		ax-1cn	$⊢ 1 \in ℂ$
4		subcl	$⊢ (1 \in ℂ \land R \in ℂ) \to 1 - R \in ℂ$
5	3 2 4	sylancr	$⊢ (A \in ℂ \land R \in ℂ \land \|R\| < 1) \to 1 - R \in ℂ$
6		simp3	$⊢ (A \in ℂ \land R \in ℂ \land \|R\| < 1) \to \|R\| < 1$
7		1re	$⊢ 1 \in ℝ$
8	7	ltnri	$⊢ \neg 1 < 1$
9		abs1	$⊢ \|1\| = 1$
10		fveq2	$⊢ 1 = R \to \|1\| = \|R\|$
11	9 10	syl5eqr	$⊢ 1 = R \to 1 = \|R\|$
12	11	breq1d	$⊢ 1 = R \to (1 < 1 \leftrightarrow \|R\| < 1)$
13	8 12	mtbii	$⊢ 1 = R \to \neg \|R\| < 1$
14	13	necon2ai	$⊢ \|R\| < 1 \to 1 \neq R$
15	6 14	syl	$⊢ (A \in ℂ \land R \in ℂ \land \|R\| < 1) \to 1 \neq R$
16		subeq0	$⊢ (1 \in ℂ \land R \in ℂ) \to (1 - R = 0 \leftrightarrow 1 = R)$
17	16	necon3bid	$⊢ (1 \in ℂ \land R \in ℂ) \to (1 - R \neq 0 \leftrightarrow 1 \neq R)$
18	3 2 17	sylancr	$⊢ (A \in ℂ \land R \in ℂ \land \|R\| < 1) \to (1 - R \neq 0 \leftrightarrow 1 \neq R)$
19	15 18	mpbird	$⊢ (A \in ℂ \land R \in ℂ \land \|R\| < 1) \to 1 - R \neq 0$
20	1 2 5 19	divassd	$⊢ (A \in ℂ \land R \in ℂ \land \|R\| < 1) \to \frac{A R}{1 - R} = A (\frac{R}{1 - R})$
21		geoisum1	$⊢ (R \in ℂ \land \|R\| < 1) \to \sum_{k \in ℕ} R^{k} = \frac{R}{1 - R}$
22	21	3adant1	$⊢ (A \in ℂ \land R \in ℂ \land \|R\| < 1) \to \sum_{k \in ℕ} R^{k} = \frac{R}{1 - R}$
23	22	oveq2d	$⊢ (A \in ℂ \land R \in ℂ \land \|R\| < 1) \to A \sum_{k \in ℕ} R^{k} = A (\frac{R}{1 - R})$
24		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
25		1zzd	$⊢ (A \in ℂ \land R \in ℂ \land \|R\| < 1) \to 1 \in ℤ$
26		oveq2	$⊢ n = k \to R^{n} = R^{k}$
27		eqid	$⊢ (n \in ℕ ⟼ R^{n}) = (n \in ℕ ⟼ R^{n})$
28		ovex	$⊢ R^{k} \in V$
29	26 27 28	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ R^{n}) (k) = R^{k}$
30	29	adantl	$⊢ ((A \in ℂ \land R \in ℂ \land \|R\| < 1) \land k \in ℕ) \to (n \in ℕ ⟼ R^{n}) (k) = R^{k}$
31		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
32		expcl	$⊢ (R \in ℂ \land k \in ℕ_{0}) \to R^{k} \in ℂ$
33	2 31 32	syl2an	$⊢ ((A \in ℂ \land R \in ℂ \land \|R\| < 1) \land k \in ℕ) \to R^{k} \in ℂ$
34		1nn0	$⊢ 1 \in ℕ_{0}$
35	34	a1i	$⊢ (A \in ℂ \land R \in ℂ \land \|R\| < 1) \to 1 \in ℕ_{0}$
36		elnnuz	$⊢ k \in ℕ \leftrightarrow k \in ℤ_{\geq 1}$
37	36 30	sylan2br	$⊢ ((A \in ℂ \land R \in ℂ \land \|R\| < 1) \land k \in ℤ_{\geq 1}) \to (n \in ℕ ⟼ R^{n}) (k) = R^{k}$
38	2 6 35 37	geolim2	$⊢ (A \in ℂ \land R \in ℂ \land \|R\| < 1) \to seq 1 (+ (n \in ℕ ⟼ R^{n})) ⇝ (\frac{R^{1}}{1 - R})$
39		seqex	$⊢ seq 1 (+ (n \in ℕ ⟼ R^{n})) \in V$
40		ovex	$⊢ \frac{R^{1}}{1 - R} \in V$
41	39 40	breldm	$⊢ seq 1 (+ (n \in ℕ ⟼ R^{n})) ⇝ (\frac{R^{1}}{1 - R}) \to seq 1 (+ (n \in ℕ ⟼ R^{n})) \in dom ⇝$
42	38 41	syl	$⊢ (A \in ℂ \land R \in ℂ \land \|R\| < 1) \to seq 1 (+ (n \in ℕ ⟼ R^{n})) \in dom ⇝$
43	24 25 30 33 42 1	isummulc2	$⊢ (A \in ℂ \land R \in ℂ \land \|R\| < 1) \to A \sum_{k \in ℕ} R^{k} = \sum_{k \in ℕ} A R^{k}$
44	20 23 43	3eqtr2rd	$⊢ (A \in ℂ \land R \in ℂ \land \|R\| < 1) \to \sum_{k \in ℕ} A R^{k} = \frac{A R}{1 - R}$

Metamath Proof Explorer

Theorem geoisum1c

Proof