geo2sum

Description: The value of the finite geometric series 2 ^ -u 1 + 2 ^ -u 2 + ... + 2 ^ -u N , multiplied by a constant. (Contributed by Mario Carneiro, 17-Mar-2014) (Revised by Mario Carneiro, 26-Apr-2014)

		Ref	Expression
	Assertion	geo2sum	$⊢ (N \in ℕ \land A \in ℂ) \to \sum_{k = 1}^{N} (\frac{A}{2^{k}}) = A - (\frac{A}{2^{N}})$

Proof

Step	Hyp	Ref	Expression
1		1zzd	$⊢ (N \in ℕ \land A \in ℂ) \to 1 \in ℤ$
2		nnz	$⊢ N \in ℕ \to N \in ℤ$
3	2	adantr	$⊢ (N \in ℕ \land A \in ℂ) \to N \in ℤ$
4		simplr	$⊢ ((N \in ℕ \land A \in ℂ) \land k \in (1 \dots N)) \to A \in ℂ$
5		2nn	$⊢ 2 \in ℕ$
6		elfznn	$⊢ k \in (1 \dots N) \to k \in ℕ$
7	6	adantl	$⊢ ((N \in ℕ \land A \in ℂ) \land k \in (1 \dots N)) \to k \in ℕ$
8	7	nnnn0d	$⊢ ((N \in ℕ \land A \in ℂ) \land k \in (1 \dots N)) \to k \in ℕ_{0}$
9		nnexpcl	$⊢ (2 \in ℕ \land k \in ℕ_{0}) \to 2^{k} \in ℕ$
10	5 8 9	sylancr	$⊢ ((N \in ℕ \land A \in ℂ) \land k \in (1 \dots N)) \to 2^{k} \in ℕ$
11	10	nncnd	$⊢ ((N \in ℕ \land A \in ℂ) \land k \in (1 \dots N)) \to 2^{k} \in ℂ$
12	10	nnne0d	$⊢ ((N \in ℕ \land A \in ℂ) \land k \in (1 \dots N)) \to 2^{k} \neq 0$
13	4 11 12	divcld	$⊢ ((N \in ℕ \land A \in ℂ) \land k \in (1 \dots N)) \to \frac{A}{2^{k}} \in ℂ$
14		oveq2	$⊢ k = j + 1 \to 2^{k} = 2^{j + 1}$
15	14	oveq2d	$⊢ k = j + 1 \to \frac{A}{2^{k}} = \frac{A}{2^{j + 1}}$
16	1 1 3 13 15	fsumshftm	$⊢ (N \in ℕ \land A \in ℂ) \to \sum_{k = 1}^{N} (\frac{A}{2^{k}}) = \sum_{j = 1 - 1}^{N - 1} (\frac{A}{2^{j + 1}})$
17		1m1e0	$⊢ 1 - 1 = 0$
18	17	oveq1i	$⊢ (1 - 1 \dots N - 1) = (0 \dots N - 1)$
19	18	sumeq1i	$⊢ \sum_{j = 1 - 1}^{N - 1} (\frac{A}{2^{j + 1}}) = \sum_{j = 0}^{N - 1} (\frac{A}{2^{j + 1}})$
20		halfcn	$⊢ \frac{1}{2} \in ℂ$
21		elfznn0	$⊢ j \in (0 \dots N - 1) \to j \in ℕ_{0}$
22	21	adantl	$⊢ ((N \in ℕ \land A \in ℂ) \land j \in (0 \dots N - 1)) \to j \in ℕ_{0}$
23		expcl	$⊢ (\frac{1}{2} \in ℂ \land j \in ℕ_{0}) \to {(\frac{1}{2})}^{j} \in ℂ$
24	20 22 23	sylancr	$⊢ ((N \in ℕ \land A \in ℂ) \land j \in (0 \dots N - 1)) \to {(\frac{1}{2})}^{j} \in ℂ$
25		2cnd	$⊢ ((N \in ℕ \land A \in ℂ) \land j \in (0 \dots N - 1)) \to 2 \in ℂ$
26		2ne0	$⊢ 2 \neq 0$
27	26	a1i	$⊢ ((N \in ℕ \land A \in ℂ) \land j \in (0 \dots N - 1)) \to 2 \neq 0$
28	24 25 27	divrecd	$⊢ ((N \in ℕ \land A \in ℂ) \land j \in (0 \dots N - 1)) \to \frac{{(\frac{1}{2})}^{j}}{2} = {(\frac{1}{2})}^{j} (\frac{1}{2})$
29		expp1	$⊢ (\frac{1}{2} \in ℂ \land j \in ℕ_{0}) \to {(\frac{1}{2})}^{j + 1} = {(\frac{1}{2})}^{j} (\frac{1}{2})$
30	20 22 29	sylancr	$⊢ ((N \in ℕ \land A \in ℂ) \land j \in (0 \dots N - 1)) \to {(\frac{1}{2})}^{j + 1} = {(\frac{1}{2})}^{j} (\frac{1}{2})$
31		elfzelz	$⊢ j \in (0 \dots N - 1) \to j \in ℤ$
32	31	peano2zd	$⊢ j \in (0 \dots N - 1) \to j + 1 \in ℤ$
33	32	adantl	$⊢ ((N \in ℕ \land A \in ℂ) \land j \in (0 \dots N - 1)) \to j + 1 \in ℤ$
34	25 27 33	exprecd	$⊢ ((N \in ℕ \land A \in ℂ) \land j \in (0 \dots N - 1)) \to {(\frac{1}{2})}^{j + 1} = \frac{1}{2^{j + 1}}$
35	28 30 34	3eqtr2rd	$⊢ ((N \in ℕ \land A \in ℂ) \land j \in (0 \dots N - 1)) \to \frac{1}{2^{j + 1}} = \frac{{(\frac{1}{2})}^{j}}{2}$
36	35	oveq2d	$⊢ ((N \in ℕ \land A \in ℂ) \land j \in (0 \dots N - 1)) \to A (\frac{1}{2^{j + 1}}) = A (\frac{{(\frac{1}{2})}^{j}}{2})$
37		simplr	$⊢ ((N \in ℕ \land A \in ℂ) \land j \in (0 \dots N - 1)) \to A \in ℂ$
38		peano2nn0	$⊢ j \in ℕ_{0} \to j + 1 \in ℕ_{0}$
39	22 38	syl	$⊢ ((N \in ℕ \land A \in ℂ) \land j \in (0 \dots N - 1)) \to j + 1 \in ℕ_{0}$
40		nnexpcl	$⊢ (2 \in ℕ \land j + 1 \in ℕ_{0}) \to 2^{j + 1} \in ℕ$
41	5 39 40	sylancr	$⊢ ((N \in ℕ \land A \in ℂ) \land j \in (0 \dots N - 1)) \to 2^{j + 1} \in ℕ$
42	41	nncnd	$⊢ ((N \in ℕ \land A \in ℂ) \land j \in (0 \dots N - 1)) \to 2^{j + 1} \in ℂ$
43	41	nnne0d	$⊢ ((N \in ℕ \land A \in ℂ) \land j \in (0 \dots N - 1)) \to 2^{j + 1} \neq 0$
44	37 42 43	divrecd	$⊢ ((N \in ℕ \land A \in ℂ) \land j \in (0 \dots N - 1)) \to \frac{A}{2^{j + 1}} = A (\frac{1}{2^{j + 1}})$
45	24 37 25 27	div12d	$⊢ ((N \in ℕ \land A \in ℂ) \land j \in (0 \dots N - 1)) \to {(\frac{1}{2})}^{j} (\frac{A}{2}) = A (\frac{{(\frac{1}{2})}^{j}}{2})$
46	36 44 45	3eqtr4d	$⊢ ((N \in ℕ \land A \in ℂ) \land j \in (0 \dots N - 1)) \to \frac{A}{2^{j + 1}} = {(\frac{1}{2})}^{j} (\frac{A}{2})$
47	46	sumeq2dv	$⊢ (N \in ℕ \land A \in ℂ) \to \sum_{j = 0}^{N - 1} (\frac{A}{2^{j + 1}}) = \sum_{j = 0}^{N - 1} {(\frac{1}{2})}^{j} (\frac{A}{2})$
48		fzfid	$⊢ (N \in ℕ \land A \in ℂ) \to (0 \dots N - 1) \in Fin$
49		halfcl	$⊢ A \in ℂ \to \frac{A}{2} \in ℂ$
50	49	adantl	$⊢ (N \in ℕ \land A \in ℂ) \to \frac{A}{2} \in ℂ$
51	48 50 24	fsummulc1	$⊢ (N \in ℕ \land A \in ℂ) \to \sum_{j = 0}^{N - 1} {(\frac{1}{2})}^{j} (\frac{A}{2}) = \sum_{j = 0}^{N - 1} {(\frac{1}{2})}^{j} (\frac{A}{2})$
52	47 51	eqtr4d	$⊢ (N \in ℕ \land A \in ℂ) \to \sum_{j = 0}^{N - 1} (\frac{A}{2^{j + 1}}) = \sum_{j = 0}^{N - 1} {(\frac{1}{2})}^{j} (\frac{A}{2})$
53	19 52	eqtrid	$⊢ (N \in ℕ \land A \in ℂ) \to \sum_{j = 1 - 1}^{N - 1} (\frac{A}{2^{j + 1}}) = \sum_{j = 0}^{N - 1} {(\frac{1}{2})}^{j} (\frac{A}{2})$
54		2cnd	$⊢ (N \in ℕ \land A \in ℂ) \to 2 \in ℂ$
55	26	a1i	$⊢ (N \in ℕ \land A \in ℂ) \to 2 \neq 0$
56	54 55 3	exprecd	$⊢ (N \in ℕ \land A \in ℂ) \to {(\frac{1}{2})}^{N} = \frac{1}{2^{N}}$
57	56	oveq2d	$⊢ (N \in ℕ \land A \in ℂ) \to 1 - {(\frac{1}{2})}^{N} = 1 - (\frac{1}{2^{N}})$
58		1mhlfehlf	$⊢ 1 - (\frac{1}{2}) = \frac{1}{2}$
59	58	a1i	$⊢ (N \in ℕ \land A \in ℂ) \to 1 - (\frac{1}{2}) = \frac{1}{2}$
60	57 59	oveq12d	$⊢ (N \in ℕ \land A \in ℂ) \to \frac{1 - {(\frac{1}{2})}^{N}}{1 - (\frac{1}{2})} = \frac{1 - (\frac{1}{2^{N}})}{\frac{1}{2}}$
61		simpr	$⊢ (N \in ℕ \land A \in ℂ) \to A \in ℂ$
62	61 54 55	divrec2d	$⊢ (N \in ℕ \land A \in ℂ) \to \frac{A}{2} = (\frac{1}{2}) A$
63	60 62	oveq12d	$⊢ (N \in ℕ \land A \in ℂ) \to (\frac{1 - {(\frac{1}{2})}^{N}}{1 - (\frac{1}{2})}) (\frac{A}{2}) = (\frac{1 - (\frac{1}{2^{N}})}{\frac{1}{2}}) (\frac{1}{2}) A$
64		ax-1cn	$⊢ 1 \in ℂ$
65		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
66	65	adantr	$⊢ (N \in ℕ \land A \in ℂ) \to N \in ℕ_{0}$
67		nnexpcl	$⊢ (2 \in ℕ \land N \in ℕ_{0}) \to 2^{N} \in ℕ$
68	5 66 67	sylancr	$⊢ (N \in ℕ \land A \in ℂ) \to 2^{N} \in ℕ$
69	68	nnrecred	$⊢ (N \in ℕ \land A \in ℂ) \to \frac{1}{2^{N}} \in ℝ$
70	69	recnd	$⊢ (N \in ℕ \land A \in ℂ) \to \frac{1}{2^{N}} \in ℂ$
71		subcl	$⊢ (1 \in ℂ \land \frac{1}{2^{N}} \in ℂ) \to 1 - (\frac{1}{2^{N}}) \in ℂ$
72	64 70 71	sylancr	$⊢ (N \in ℕ \land A \in ℂ) \to 1 - (\frac{1}{2^{N}}) \in ℂ$
73	20	a1i	$⊢ (N \in ℕ \land A \in ℂ) \to \frac{1}{2} \in ℂ$
74		0re	$⊢ 0 \in ℝ$
75		halfgt0	$⊢ 0 < \frac{1}{2}$
76	74 75	gtneii	$⊢ \frac{1}{2} \neq 0$
77	76	a1i	$⊢ (N \in ℕ \land A \in ℂ) \to \frac{1}{2} \neq 0$
78	72 73 77	divcld	$⊢ (N \in ℕ \land A \in ℂ) \to \frac{1 - (\frac{1}{2^{N}})}{\frac{1}{2}} \in ℂ$
79	78 73 61	mulassd	$⊢ (N \in ℕ \land A \in ℂ) \to (\frac{1 - (\frac{1}{2^{N}})}{\frac{1}{2}}) (\frac{1}{2}) A = (\frac{1 - (\frac{1}{2^{N}})}{\frac{1}{2}}) (\frac{1}{2}) A$
80	72 73 77	divcan1d	$⊢ (N \in ℕ \land A \in ℂ) \to (\frac{1 - (\frac{1}{2^{N}})}{\frac{1}{2}}) (\frac{1}{2}) = 1 - (\frac{1}{2^{N}})$
81	80	oveq1d	$⊢ (N \in ℕ \land A \in ℂ) \to (\frac{1 - (\frac{1}{2^{N}})}{\frac{1}{2}}) (\frac{1}{2}) A = (1 - (\frac{1}{2^{N}})) A$
82	63 79 81	3eqtr2d	$⊢ (N \in ℕ \land A \in ℂ) \to (\frac{1 - {(\frac{1}{2})}^{N}}{1 - (\frac{1}{2})}) (\frac{A}{2}) = (1 - (\frac{1}{2^{N}})) A$
83		halfre	$⊢ \frac{1}{2} \in ℝ$
84		halflt1	$⊢ \frac{1}{2} < 1$
85	83 84	ltneii	$⊢ \frac{1}{2} \neq 1$
86	85	a1i	$⊢ (N \in ℕ \land A \in ℂ) \to \frac{1}{2} \neq 1$
87	73 86 66	geoser	$⊢ (N \in ℕ \land A \in ℂ) \to \sum_{j = 0}^{N - 1} {(\frac{1}{2})}^{j} = \frac{1 - {(\frac{1}{2})}^{N}}{1 - (\frac{1}{2})}$
88	87	oveq1d	$⊢ (N \in ℕ \land A \in ℂ) \to \sum_{j = 0}^{N - 1} {(\frac{1}{2})}^{j} (\frac{A}{2}) = (\frac{1 - {(\frac{1}{2})}^{N}}{1 - (\frac{1}{2})}) (\frac{A}{2})$
89		mullid	$⊢ A \in ℂ \to 1 A = A$
90	89	adantl	$⊢ (N \in ℕ \land A \in ℂ) \to 1 A = A$
91	90	eqcomd	$⊢ (N \in ℕ \land A \in ℂ) \to A = 1 A$
92	68	nncnd	$⊢ (N \in ℕ \land A \in ℂ) \to 2^{N} \in ℂ$
93	68	nnne0d	$⊢ (N \in ℕ \land A \in ℂ) \to 2^{N} \neq 0$
94	61 92 93	divrec2d	$⊢ (N \in ℕ \land A \in ℂ) \to \frac{A}{2^{N}} = (\frac{1}{2^{N}}) A$
95	91 94	oveq12d	$⊢ (N \in ℕ \land A \in ℂ) \to A - (\frac{A}{2^{N}}) = 1 A - (\frac{1}{2^{N}}) A$
96	64	a1i	$⊢ (N \in ℕ \land A \in ℂ) \to 1 \in ℂ$
97	96 70 61	subdird	$⊢ (N \in ℕ \land A \in ℂ) \to (1 - (\frac{1}{2^{N}})) A = 1 A - (\frac{1}{2^{N}}) A$
98	95 97	eqtr4d	$⊢ (N \in ℕ \land A \in ℂ) \to A - (\frac{A}{2^{N}}) = (1 - (\frac{1}{2^{N}})) A$
99	82 88 98	3eqtr4d	$⊢ (N \in ℕ \land A \in ℂ) \to \sum_{j = 0}^{N - 1} {(\frac{1}{2})}^{j} (\frac{A}{2}) = A - (\frac{A}{2^{N}})$
100	16 53 99	3eqtrd	$⊢ (N \in ℕ \land A \in ℂ) \to \sum_{k = 1}^{N} (\frac{A}{2^{k}}) = A - (\frac{A}{2^{N}})$

Metamath Proof Explorer

Theorem geo2sum

Proof