geo2lim

Description: The value of the infinite geometric series 2 ^ -u 1 + 2 ^ -u 2 + ... , multiplied by a constant. (Contributed by Mario Carneiro, 15-Jun-2014)

		Ref	Expression
	Hypothesis	geo2lim.1	$⊢ F = (k \in ℕ ⟼ \frac{A}{2^{k}})$
	Assertion	geo2lim	$⊢ A \in ℂ \to seq 1 (+ F) ⇝ A$

Proof

Step	Hyp	Ref	Expression
1		geo2lim.1	$⊢ F = (k \in ℕ ⟼ \frac{A}{2^{k}})$
2		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
3		1zzd	$⊢ A \in ℂ \to 1 \in ℤ$
4		halfcn	$⊢ \frac{1}{2} \in ℂ$
5	4	a1i	$⊢ A \in ℂ \to \frac{1}{2} \in ℂ$
6		halfre	$⊢ \frac{1}{2} \in ℝ$
7		halfge0	$⊢ 0 \leq \frac{1}{2}$
8		absid	$⊢ (\frac{1}{2} \in ℝ \land 0 \leq \frac{1}{2}) \to \|\frac{1}{2}\| = \frac{1}{2}$
9	6 7 8	mp2an	$⊢ \|\frac{1}{2}\| = \frac{1}{2}$
10		halflt1	$⊢ \frac{1}{2} < 1$
11	9 10	eqbrtri	$⊢ \|\frac{1}{2}\| < 1$
12	11	a1i	$⊢ A \in ℂ \to \|\frac{1}{2}\| < 1$
13	5 12	expcnv	$⊢ A \in ℂ \to (k \in ℕ_{0} ⟼ {(\frac{1}{2})}^{k}) ⇝ 0$
14		id	$⊢ A \in ℂ \to A \in ℂ$
15		nnex	$⊢ ℕ \in V$
16	15	mptex	$⊢ (k \in ℕ ⟼ \frac{A}{2^{k}}) \in V$
17	1 16	eqeltri	$⊢ F \in V$
18	17	a1i	$⊢ A \in ℂ \to F \in V$
19		nnnn0	$⊢ j \in ℕ \to j \in ℕ_{0}$
20	19	adantl	$⊢ (A \in ℂ \land j \in ℕ) \to j \in ℕ_{0}$
21		oveq2	$⊢ k = j \to {(\frac{1}{2})}^{k} = {(\frac{1}{2})}^{j}$
22		eqid	$⊢ (k \in ℕ_{0} ⟼ {(\frac{1}{2})}^{k}) = (k \in ℕ_{0} ⟼ {(\frac{1}{2})}^{k})$
23		ovex	$⊢ {(\frac{1}{2})}^{j} \in V$
24	21 22 23	fvmpt	$⊢ j \in ℕ_{0} \to (k \in ℕ_{0} ⟼ {(\frac{1}{2})}^{k}) (j) = {(\frac{1}{2})}^{j}$
25	20 24	syl	$⊢ (A \in ℂ \land j \in ℕ) \to (k \in ℕ_{0} ⟼ {(\frac{1}{2})}^{k}) (j) = {(\frac{1}{2})}^{j}$
26		2cn	$⊢ 2 \in ℂ$
27		2ne0	$⊢ 2 \neq 0$
28		nnz	$⊢ j \in ℕ \to j \in ℤ$
29	28	adantl	$⊢ (A \in ℂ \land j \in ℕ) \to j \in ℤ$
30		exprec	$⊢ (2 \in ℂ \land 2 \neq 0 \land j \in ℤ) \to {(\frac{1}{2})}^{j} = \frac{1}{2^{j}}$
31	26 27 29 30	mp3an12i	$⊢ (A \in ℂ \land j \in ℕ) \to {(\frac{1}{2})}^{j} = \frac{1}{2^{j}}$
32	25 31	eqtrd	$⊢ (A \in ℂ \land j \in ℕ) \to (k \in ℕ_{0} ⟼ {(\frac{1}{2})}^{k}) (j) = \frac{1}{2^{j}}$
33		2nn	$⊢ 2 \in ℕ$
34		nnexpcl	$⊢ (2 \in ℕ \land j \in ℕ_{0}) \to 2^{j} \in ℕ$
35	33 20 34	sylancr	$⊢ (A \in ℂ \land j \in ℕ) \to 2^{j} \in ℕ$
36	35	nnrecred	$⊢ (A \in ℂ \land j \in ℕ) \to \frac{1}{2^{j}} \in ℝ$
37	36	recnd	$⊢ (A \in ℂ \land j \in ℕ) \to \frac{1}{2^{j}} \in ℂ$
38	32 37	eqeltrd	$⊢ (A \in ℂ \land j \in ℕ) \to (k \in ℕ_{0} ⟼ {(\frac{1}{2})}^{k}) (j) \in ℂ$
39		simpl	$⊢ (A \in ℂ \land j \in ℕ) \to A \in ℂ$
40	35	nncnd	$⊢ (A \in ℂ \land j \in ℕ) \to 2^{j} \in ℂ$
41	35	nnne0d	$⊢ (A \in ℂ \land j \in ℕ) \to 2^{j} \neq 0$
42	39 40 41	divrecd	$⊢ (A \in ℂ \land j \in ℕ) \to \frac{A}{2^{j}} = A (\frac{1}{2^{j}})$
43		oveq2	$⊢ k = j \to 2^{k} = 2^{j}$
44	43	oveq2d	$⊢ k = j \to \frac{A}{2^{k}} = \frac{A}{2^{j}}$
45		ovex	$⊢ \frac{A}{2^{j}} \in V$
46	44 1 45	fvmpt	$⊢ j \in ℕ \to F (j) = \frac{A}{2^{j}}$
47	46	adantl	$⊢ (A \in ℂ \land j \in ℕ) \to F (j) = \frac{A}{2^{j}}$
48	32	oveq2d	$⊢ (A \in ℂ \land j \in ℕ) \to A (k \in ℕ_{0} ⟼ {(\frac{1}{2})}^{k}) (j) = A (\frac{1}{2^{j}})$
49	42 47 48	3eqtr4d	$⊢ (A \in ℂ \land j \in ℕ) \to F (j) = A (k \in ℕ_{0} ⟼ {(\frac{1}{2})}^{k}) (j)$
50	2 3 13 14 18 38 49	climmulc2	$⊢ A \in ℂ \to F ⇝ A \cdot 0$
51		mul01	$⊢ A \in ℂ \to A \cdot 0 = 0$
52	50 51	breqtrd	$⊢ A \in ℂ \to F ⇝ 0$
53		seqex	$⊢ seq 1 (+ F) \in V$
54	53	a1i	$⊢ A \in ℂ \to seq 1 (+ F) \in V$
55	39 40 41	divcld	$⊢ (A \in ℂ \land j \in ℕ) \to \frac{A}{2^{j}} \in ℂ$
56	47 55	eqeltrd	$⊢ (A \in ℂ \land j \in ℕ) \to F (j) \in ℂ$
57	47	oveq2d	$⊢ (A \in ℂ \land j \in ℕ) \to A - F (j) = A - (\frac{A}{2^{j}})$
58		geo2sum	$⊢ (j \in ℕ \land A \in ℂ) \to \sum_{n = 1}^{j} (\frac{A}{2^{n}}) = A - (\frac{A}{2^{j}})$
59	58	ancoms	$⊢ (A \in ℂ \land j \in ℕ) \to \sum_{n = 1}^{j} (\frac{A}{2^{n}}) = A - (\frac{A}{2^{j}})$
60		elfznn	$⊢ n \in (1 \dots j) \to n \in ℕ$
61	60	adantl	$⊢ ((A \in ℂ \land j \in ℕ) \land n \in (1 \dots j)) \to n \in ℕ$
62		oveq2	$⊢ k = n \to 2^{k} = 2^{n}$
63	62	oveq2d	$⊢ k = n \to \frac{A}{2^{k}} = \frac{A}{2^{n}}$
64		ovex	$⊢ \frac{A}{2^{n}} \in V$
65	63 1 64	fvmpt	$⊢ n \in ℕ \to F (n) = \frac{A}{2^{n}}$
66	61 65	syl	$⊢ ((A \in ℂ \land j \in ℕ) \land n \in (1 \dots j)) \to F (n) = \frac{A}{2^{n}}$
67		simpr	$⊢ (A \in ℂ \land j \in ℕ) \to j \in ℕ$
68	67 2	eleqtrdi	$⊢ (A \in ℂ \land j \in ℕ) \to j \in ℤ_{\geq 1}$
69		simpll	$⊢ ((A \in ℂ \land j \in ℕ) \land n \in (1 \dots j)) \to A \in ℂ$
70		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
71		nnexpcl	$⊢ (2 \in ℕ \land n \in ℕ_{0}) \to 2^{n} \in ℕ$
72	33 70 71	sylancr	$⊢ n \in ℕ \to 2^{n} \in ℕ$
73	61 72	syl	$⊢ ((A \in ℂ \land j \in ℕ) \land n \in (1 \dots j)) \to 2^{n} \in ℕ$
74	73	nncnd	$⊢ ((A \in ℂ \land j \in ℕ) \land n \in (1 \dots j)) \to 2^{n} \in ℂ$
75	73	nnne0d	$⊢ ((A \in ℂ \land j \in ℕ) \land n \in (1 \dots j)) \to 2^{n} \neq 0$
76	69 74 75	divcld	$⊢ ((A \in ℂ \land j \in ℕ) \land n \in (1 \dots j)) \to \frac{A}{2^{n}} \in ℂ$
77	66 68 76	fsumser	$⊢ (A \in ℂ \land j \in ℕ) \to \sum_{n = 1}^{j} (\frac{A}{2^{n}}) = seq 1 (+ F) (j)$
78	57 59 77	3eqtr2rd	$⊢ (A \in ℂ \land j \in ℕ) \to seq 1 (+ F) (j) = A - F (j)$
79	2 3 52 14 54 56 78	climsubc2	$⊢ A \in ℂ \to seq 1 (+ F) ⇝ (A - 0)$
80		subid1	$⊢ A \in ℂ \to A - 0 = A$
81	79 80	breqtrd	$⊢ A \in ℂ \to seq 1 (+ F) ⇝ A$

Metamath Proof Explorer

Theorem geo2lim

Proof