fsumparts

Description: Summation by parts. (Contributed by Mario Carneiro, 13-Apr-2016)

	Ref	Expression
Hypotheses	fsumparts.b	$⊢ k = j \to (A = B \land V = W)$
	fsumparts.c	$⊢ k = j + 1 \to (A = C \land V = X)$
	fsumparts.d	$⊢ k = M \to (A = D \land V = Y)$
	fsumparts.e	$⊢ k = N \to (A = E \land V = Z)$
	fsumparts.1	$⊢ φ \to N \in ℤ_{\geq M}$
	fsumparts.2	$⊢ (φ \land k \in (M \dots N)) \to A \in ℂ$
	fsumparts.3	$⊢ (φ \land k \in (M \dots N)) \to V \in ℂ$
Assertion	fsumparts	$⊢ φ \to \sum_{j \in (M ..^N)} B (X - W) = E Z - D Y - \sum_{j \in (M ..^N)} (C - B) X$

Proof

Step	Hyp	Ref	Expression
1		fsumparts.b	$⊢ k = j \to (A = B \land V = W)$
2		fsumparts.c	$⊢ k = j + 1 \to (A = C \land V = X)$
3		fsumparts.d	$⊢ k = M \to (A = D \land V = Y)$
4		fsumparts.e	$⊢ k = N \to (A = E \land V = Z)$
5		fsumparts.1	$⊢ φ \to N \in ℤ_{\geq M}$
6		fsumparts.2	$⊢ (φ \land k \in (M \dots N)) \to A \in ℂ$
7		fsumparts.3	$⊢ (φ \land k \in (M \dots N)) \to V \in ℂ$
8		sum0	$⊢ \sum_{j \in \emptyset} B (X - W) = 0$
9		0m0e0	$⊢ 0 - 0 = 0$
10	8 9	eqtr4i	$⊢ \sum_{j \in \emptyset} B (X - W) = 0 - 0$
11		simpr	$⊢ (φ \land N = M) \to N = M$
12	11	oveq2d	$⊢ (φ \land N = M) \to (M ..^N) = (M ..^M)$
13		fzo0	$⊢ (M ..^M) = \emptyset$
14	12 13	eqtrdi	$⊢ (φ \land N = M) \to (M ..^N) = \emptyset$
15	14	sumeq1d	$⊢ (φ \land N = M) \to \sum_{j \in (M ..^N)} B (X - W) = \sum_{j \in \emptyset} B (X - W)$
16		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
17	5 16	syl	$⊢ φ \to M \in (M \dots N)$
18		eqtr3	$⊢ (k = M \land N = M) \to k = N$
19		oveq12	$⊢ (A = E \land V = Z) \to A V = E Z$
20	18 4 19	3syl	$⊢ (k = M \land N = M) \to A V = E Z$
21		oveq12	$⊢ (A = D \land V = Y) \to A V = D Y$
22	3 21	syl	$⊢ k = M \to A V = D Y$
23	22	adantr	$⊢ (k = M \land N = M) \to A V = D Y$
24	20 23	eqeq12d	$⊢ (k = M \land N = M) \to (A V = A V \leftrightarrow E Z = D Y)$
25	24	pm5.74da	$⊢ k = M \to ((N = M \to A V = A V) \leftrightarrow (N = M \to E Z = D Y))$
26		eqidd	$⊢ N = M \to A V = A V$
27	25 26	vtoclg	$⊢ M \in (M \dots N) \to (N = M \to E Z = D Y)$
28	27	imp	$⊢ (M \in (M \dots N) \land N = M) \to E Z = D Y$
29	17 28	sylan	$⊢ (φ \land N = M) \to E Z = D Y$
30	29	oveq1d	$⊢ (φ \land N = M) \to E Z - D Y = D Y - D Y$
31	3	simpld	$⊢ k = M \to A = D$
32	31	eleq1d	$⊢ k = M \to (A \in ℂ \leftrightarrow D \in ℂ)$
33	6	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) A \in ℂ$
34	32 33 17	rspcdva	$⊢ φ \to D \in ℂ$
35	3	simprd	$⊢ k = M \to V = Y$
36	35	eleq1d	$⊢ k = M \to (V \in ℂ \leftrightarrow Y \in ℂ)$
37	7	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) V \in ℂ$
38	36 37 17	rspcdva	$⊢ φ \to Y \in ℂ$
39	34 38	mulcld	$⊢ φ \to D Y \in ℂ$
40	39	subidd	$⊢ φ \to D Y - D Y = 0$
41	40	adantr	$⊢ (φ \land N = M) \to D Y - D Y = 0$
42	30 41	eqtrd	$⊢ (φ \land N = M) \to E Z - D Y = 0$
43	14	sumeq1d	$⊢ (φ \land N = M) \to \sum_{j \in (M ..^N)} (C - B) X = \sum_{j \in \emptyset} (C - B) X$
44		sum0	$⊢ \sum_{j \in \emptyset} (C - B) X = 0$
45	43 44	eqtrdi	$⊢ (φ \land N = M) \to \sum_{j \in (M ..^N)} (C - B) X = 0$
46	42 45	oveq12d	$⊢ (φ \land N = M) \to E Z - D Y - \sum_{j \in (M ..^N)} (C - B) X = 0 - 0$
47	10 15 46	3eqtr4a	$⊢ (φ \land N = M) \to \sum_{j \in (M ..^N)} B (X - W) = E Z - D Y - \sum_{j \in (M ..^N)} (C - B) X$
48		fzofi	$⊢ (M + 1 ..^N) \in Fin$
49	48	a1i	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to (M + 1 ..^N) \in Fin$
50		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
51	5 50	syl	$⊢ φ \to M \in ℤ$
52	51	adantr	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to M \in ℤ$
53		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
54		peano2uz	$⊢ M \in ℤ_{\geq M} \to M + 1 \in ℤ_{\geq M}$
55		fzoss1	$⊢ M + 1 \in ℤ_{\geq M} \to (M + 1 ..^N) \subseteq (M ..^N)$
56	52 53 54 55	4syl	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to (M + 1 ..^N) \subseteq (M ..^N)$
57	56	sselda	$⊢ ((φ \land N \in ℤ_{\geq (M + 1)}) \land k \in (M + 1 ..^N)) \to k \in (M ..^N)$
58		elfzofz	$⊢ k \in (M ..^N) \to k \in (M \dots N)$
59	6 7	mulcld	$⊢ (φ \land k \in (M \dots N)) \to A V \in ℂ$
60	58 59	sylan2	$⊢ (φ \land k \in (M ..^N)) \to A V \in ℂ$
61	60	adantlr	$⊢ ((φ \land N \in ℤ_{\geq (M + 1)}) \land k \in (M ..^N)) \to A V \in ℂ$
62	57 61	syldan	$⊢ ((φ \land N \in ℤ_{\geq (M + 1)}) \land k \in (M + 1 ..^N)) \to A V \in ℂ$
63	49 62	fsumcl	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k \in (M + 1 ..^N)} A V \in ℂ$
64	4	simpld	$⊢ k = N \to A = E$
65	64	eleq1d	$⊢ k = N \to (A \in ℂ \leftrightarrow E \in ℂ)$
66		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
67	5 66	syl	$⊢ φ \to N \in (M \dots N)$
68	65 33 67	rspcdva	$⊢ φ \to E \in ℂ$
69	4	simprd	$⊢ k = N \to V = Z$
70	69	eleq1d	$⊢ k = N \to (V \in ℂ \leftrightarrow Z \in ℂ)$
71	70 37 67	rspcdva	$⊢ φ \to Z \in ℂ$
72	68 71	mulcld	$⊢ φ \to E Z \in ℂ$
73	72	adantr	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to E Z \in ℂ$
74		simpr	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to N \in ℤ_{\geq (M + 1)}$
75		fzp1ss	$⊢ M \in ℤ \to (M + 1 \dots N) \subseteq (M \dots N)$
76	52 75	syl	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to (M + 1 \dots N) \subseteq (M \dots N)$
77	76	sselda	$⊢ ((φ \land N \in ℤ_{\geq (M + 1)}) \land k \in (M + 1 \dots N)) \to k \in (M \dots N)$
78	59	adantlr	$⊢ ((φ \land N \in ℤ_{\geq (M + 1)}) \land k \in (M \dots N)) \to A V \in ℂ$
79	77 78	syldan	$⊢ ((φ \land N \in ℤ_{\geq (M + 1)}) \land k \in (M + 1 \dots N)) \to A V \in ℂ$
80	4 19	syl	$⊢ k = N \to A V = E Z$
81	74 79 80	fsumm1	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k = M + 1}^{N} A V = \sum_{k = M + 1}^{N - 1} A V + E Z$
82		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
83	5 82	syl	$⊢ φ \to N \in ℤ$
84	83	adantr	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to N \in ℤ$
85		fzoval	$⊢ N \in ℤ \to (M ..^N) = (M \dots N - 1)$
86	84 85	syl	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to (M ..^N) = (M \dots N - 1)$
87	52	zcnd	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to M \in ℂ$
88		ax-1cn	$⊢ 1 \in ℂ$
89		pncan	$⊢ (M \in ℂ \land 1 \in ℂ) \to M + 1 - 1 = M$
90	87 88 89	sylancl	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to M + 1 - 1 = M$
91	90	oveq1d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to (M + 1 - 1 \dots N - 1) = (M \dots N - 1)$
92	86 91	eqtr4d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to (M ..^N) = (M + 1 - 1 \dots N - 1)$
93	92	sumeq1d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} C X = \sum_{j = M + 1 - 1}^{N - 1} C X$
94		1zzd	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to 1 \in ℤ$
95	52	peano2zd	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to M + 1 \in ℤ$
96		oveq12	$⊢ (A = C \land V = X) \to A V = C X$
97	2 96	syl	$⊢ k = j + 1 \to A V = C X$
98	94 95 84 79 97	fsumshftm	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k = M + 1}^{N} A V = \sum_{j = M + 1 - 1}^{N - 1} C X$
99	93 98	eqtr4d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} C X = \sum_{k = M + 1}^{N} A V$
100		fzoval	$⊢ N \in ℤ \to (M + 1 ..^N) = (M + 1 \dots N - 1)$
101	84 100	syl	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to (M + 1 ..^N) = (M + 1 \dots N - 1)$
102	101	sumeq1d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k \in (M + 1 ..^N)} A V = \sum_{k = M + 1}^{N - 1} A V$
103	102	oveq1d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k \in (M + 1 ..^N)} A V + E Z = \sum_{k = M + 1}^{N - 1} A V + E Z$
104	81 99 103	3eqtr4d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} C X = \sum_{k \in (M + 1 ..^N)} A V + E Z$
105	63 73 104	comraddd	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} C X = E Z + \sum_{k \in (M + 1 ..^N)} A V$
106	105	oveq1d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} C X - \sum_{j \in (M ..^N)} B X = E Z + \sum_{k \in (M + 1 ..^N)} A V - \sum_{j \in (M ..^N)} B X$
107		fzofzp1	$⊢ j \in (M ..^N) \to j + 1 \in (M \dots N)$
108	2	simpld	$⊢ k = j + 1 \to A = C$
109	108	eleq1d	$⊢ k = j + 1 \to (A \in ℂ \leftrightarrow C \in ℂ)$
110	109	rspccva	$⊢ (\forall k \in (M \dots N) A \in ℂ \land j + 1 \in (M \dots N)) \to C \in ℂ$
111	33 107 110	syl2an	$⊢ (φ \land j \in (M ..^N)) \to C \in ℂ$
112		elfzofz	$⊢ j \in (M ..^N) \to j \in (M \dots N)$
113	1	simpld	$⊢ k = j \to A = B$
114	113	eleq1d	$⊢ k = j \to (A \in ℂ \leftrightarrow B \in ℂ)$
115	114	rspccva	$⊢ (\forall k \in (M \dots N) A \in ℂ \land j \in (M \dots N)) \to B \in ℂ$
116	33 112 115	syl2an	$⊢ (φ \land j \in (M ..^N)) \to B \in ℂ$
117	2	simprd	$⊢ k = j + 1 \to V = X$
118	117	eleq1d	$⊢ k = j + 1 \to (V \in ℂ \leftrightarrow X \in ℂ)$
119	118	rspccva	$⊢ (\forall k \in (M \dots N) V \in ℂ \land j + 1 \in (M \dots N)) \to X \in ℂ$
120	37 107 119	syl2an	$⊢ (φ \land j \in (M ..^N)) \to X \in ℂ$
121	111 116 120	subdird	$⊢ (φ \land j \in (M ..^N)) \to (C - B) X = C X - B X$
122	121	sumeq2dv	$⊢ φ \to \sum_{j \in (M ..^N)} (C - B) X = \sum_{j \in (M ..^N)} (C X - B X)$
123		fzofi	$⊢ (M ..^N) \in Fin$
124	123	a1i	$⊢ φ \to (M ..^N) \in Fin$
125	111 120	mulcld	$⊢ (φ \land j \in (M ..^N)) \to C X \in ℂ$
126	116 120	mulcld	$⊢ (φ \land j \in (M ..^N)) \to B X \in ℂ$
127	124 125 126	fsumsub	$⊢ φ \to \sum_{j \in (M ..^N)} (C X - B X) = \sum_{j \in (M ..^N)} C X - \sum_{j \in (M ..^N)} B X$
128	122 127	eqtrd	$⊢ φ \to \sum_{j \in (M ..^N)} (C - B) X = \sum_{j \in (M ..^N)} C X - \sum_{j \in (M ..^N)} B X$
129	128	adantr	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} (C - B) X = \sum_{j \in (M ..^N)} C X - \sum_{j \in (M ..^N)} B X$
130	124 126	fsumcl	$⊢ φ \to \sum_{j \in (M ..^N)} B X \in ℂ$
131	130	adantr	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} B X \in ℂ$
132	73 131 63	subsub3d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to E Z - (\sum_{j \in (M ..^N)} B X - \sum_{k \in (M + 1 ..^N)} A V) = E Z + \sum_{k \in (M + 1 ..^N)} A V - \sum_{j \in (M ..^N)} B X$
133	106 129 132	3eqtr4d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} (C - B) X = E Z - (\sum_{j \in (M ..^N)} B X - \sum_{k \in (M + 1 ..^N)} A V)$
134	133	oveq2d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to E Z - D Y - \sum_{j \in (M ..^N)} (C - B) X = E Z - D Y - (E Z - (\sum_{j \in (M ..^N)} B X - \sum_{k \in (M + 1 ..^N)} A V))$
135	39	adantr	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to D Y \in ℂ$
136	131 63	subcld	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} B X - \sum_{k \in (M + 1 ..^N)} A V \in ℂ$
137	73 135 136	nnncan1d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to E Z - D Y - (E Z - (\sum_{j \in (M ..^N)} B X - \sum_{k \in (M + 1 ..^N)} A V)) = \sum_{j \in (M ..^N)} B X - \sum_{k \in (M + 1 ..^N)} A V - D Y$
138	63 135	addcomd	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k \in (M + 1 ..^N)} A V + D Y = D Y + \sum_{k \in (M + 1 ..^N)} A V$
139		eluzp1m1	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to N - 1 \in ℤ_{\geq M}$
140	51 139	sylan	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to N - 1 \in ℤ_{\geq M}$
141	86	eleq2d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to (k \in (M ..^N) \leftrightarrow k \in (M \dots N - 1))$
142	141	biimpar	$⊢ ((φ \land N \in ℤ_{\geq (M + 1)}) \land k \in (M \dots N - 1)) \to k \in (M ..^N)$
143	142 61	syldan	$⊢ ((φ \land N \in ℤ_{\geq (M + 1)}) \land k \in (M \dots N - 1)) \to A V \in ℂ$
144	140 143 22	fsum1p	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k = M}^{N - 1} A V = D Y + \sum_{k = M + 1}^{N - 1} A V$
145	86	sumeq1d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k \in (M ..^N)} A V = \sum_{k = M}^{N - 1} A V$
146	102	oveq2d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to D Y + \sum_{k \in (M + 1 ..^N)} A V = D Y + \sum_{k = M + 1}^{N - 1} A V$
147	144 145 146	3eqtr4d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k \in (M ..^N)} A V = D Y + \sum_{k \in (M + 1 ..^N)} A V$
148	138 147	eqtr4d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k \in (M + 1 ..^N)} A V + D Y = \sum_{k \in (M ..^N)} A V$
149		oveq12	$⊢ (A = B \land V = W) \to A V = B W$
150	1 149	syl	$⊢ k = j \to A V = B W$
151	150	cbvsumv	$⊢ \sum_{k \in (M ..^N)} A V = \sum_{j \in (M ..^N)} B W$
152	148 151	eqtrdi	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k \in (M + 1 ..^N)} A V + D Y = \sum_{j \in (M ..^N)} B W$
153	152	oveq2d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} B X - (\sum_{k \in (M + 1 ..^N)} A V + D Y) = \sum_{j \in (M ..^N)} B X - \sum_{j \in (M ..^N)} B W$
154	131 63 135	subsub4d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} B X - \sum_{k \in (M + 1 ..^N)} A V - D Y = \sum_{j \in (M ..^N)} B X - (\sum_{k \in (M + 1 ..^N)} A V + D Y)$
155	1	simprd	$⊢ k = j \to V = W$
156	155	eleq1d	$⊢ k = j \to (V \in ℂ \leftrightarrow W \in ℂ)$
157	156	rspccva	$⊢ (\forall k \in (M \dots N) V \in ℂ \land j \in (M \dots N)) \to W \in ℂ$
158	37 112 157	syl2an	$⊢ (φ \land j \in (M ..^N)) \to W \in ℂ$
159	116 120 158	subdid	$⊢ (φ \land j \in (M ..^N)) \to B (X - W) = B X - B W$
160	159	sumeq2dv	$⊢ φ \to \sum_{j \in (M ..^N)} B (X - W) = \sum_{j \in (M ..^N)} (B X - B W)$
161	116 158	mulcld	$⊢ (φ \land j \in (M ..^N)) \to B W \in ℂ$
162	124 126 161	fsumsub	$⊢ φ \to \sum_{j \in (M ..^N)} (B X - B W) = \sum_{j \in (M ..^N)} B X - \sum_{j \in (M ..^N)} B W$
163	160 162	eqtrd	$⊢ φ \to \sum_{j \in (M ..^N)} B (X - W) = \sum_{j \in (M ..^N)} B X - \sum_{j \in (M ..^N)} B W$
164	163	adantr	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} B (X - W) = \sum_{j \in (M ..^N)} B X - \sum_{j \in (M ..^N)} B W$
165	153 154 164	3eqtr4d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} B X - \sum_{k \in (M + 1 ..^N)} A V - D Y = \sum_{j \in (M ..^N)} B (X - W)$
166	134 137 165	3eqtrrd	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} B (X - W) = E Z - D Y - \sum_{j \in (M ..^N)} (C - B) X$
167		uzp1	$⊢ N \in ℤ_{\geq M} \to (N = M \lor N \in ℤ_{\geq (M + 1)})$
168	5 167	syl	$⊢ φ \to (N = M \lor N \in ℤ_{\geq (M + 1)})$
169	47 166 168	mpjaodan	$⊢ φ \to \sum_{j \in (M ..^N)} B (X - W) = E Z - D Y - \sum_{j \in (M ..^N)} (C - B) X$

Metamath Proof Explorer

Theorem fsumparts

Proof