telfsumo

Description: Sum of a telescoping series, using half-open intervals. (Contributed by Mario Carneiro, 2-May-2016)

	Ref	Expression
Hypotheses	telfsumo.1	$⊢ k = j \to A = B$
	telfsumo.2	$⊢ k = j + 1 \to A = C$
	telfsumo.3	$⊢ k = M \to A = D$
	telfsumo.4	$⊢ k = N \to A = E$
	telfsumo.5	$⊢ φ \to N \in ℤ_{\geq M}$
	telfsumo.6	$⊢ (φ \land k \in (M \dots N)) \to A \in ℂ$
Assertion	telfsumo	$⊢ φ \to \sum_{j \in (M ..^N)} (B - C) = D - E$

Proof

Step	Hyp	Ref	Expression
1		telfsumo.1	$⊢ k = j \to A = B$
2		telfsumo.2	$⊢ k = j + 1 \to A = C$
3		telfsumo.3	$⊢ k = M \to A = D$
4		telfsumo.4	$⊢ k = N \to A = E$
5		telfsumo.5	$⊢ φ \to N \in ℤ_{\geq M}$
6		telfsumo.6	$⊢ (φ \land k \in (M \dots N)) \to A \in ℂ$
7		sum0	$⊢ \sum_{j \in \emptyset} (B - C) = 0$
8	3	eleq1d	$⊢ k = M \to (A \in ℂ \leftrightarrow D \in ℂ)$
9	6	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) A \in ℂ$
10		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
11	5 10	syl	$⊢ φ \to M \in (M \dots N)$
12	8 9 11	rspcdva	$⊢ φ \to D \in ℂ$
13	12	adantr	$⊢ (φ \land N = M) \to D \in ℂ$
14	13	subidd	$⊢ (φ \land N = M) \to D - D = 0$
15	7 14	eqtr4id	$⊢ (φ \land N = M) \to \sum_{j \in \emptyset} (B - C) = D - D$
16		oveq2	$⊢ N = M \to (M ..^N) = (M ..^M)$
17	16	adantl	$⊢ (φ \land N = M) \to (M ..^N) = (M ..^M)$
18		fzo0	$⊢ (M ..^M) = \emptyset$
19	17 18	eqtrdi	$⊢ (φ \land N = M) \to (M ..^N) = \emptyset$
20	19	sumeq1d	$⊢ (φ \land N = M) \to \sum_{j \in (M ..^N)} (B - C) = \sum_{j \in \emptyset} (B - C)$
21		eqeq1	$⊢ k = N \to (k = M \leftrightarrow N = M)$
22	4	eqeq1d	$⊢ k = N \to (A = D \leftrightarrow E = D)$
23	21 22	imbi12d	$⊢ k = N \to ((k = M \to A = D) \leftrightarrow (N = M \to E = D))$
24	23 3	vtoclg	$⊢ N \in ℤ_{\geq M} \to (N = M \to E = D)$
25	24	imp	$⊢ (N \in ℤ_{\geq M} \land N = M) \to E = D$
26	5 25	sylan	$⊢ (φ \land N = M) \to E = D$
27	26	oveq2d	$⊢ (φ \land N = M) \to D - E = D - D$
28	15 20 27	3eqtr4d	$⊢ (φ \land N = M) \to \sum_{j \in (M ..^N)} (B - C) = D - E$
29		fzofi	$⊢ (M ..^N) \in Fin$
30	29	a1i	$⊢ φ \to (M ..^N) \in Fin$
31	1	eleq1d	$⊢ k = j \to (A \in ℂ \leftrightarrow B \in ℂ)$
32	9	adantr	$⊢ (φ \land j \in (M ..^N)) \to \forall k \in (M \dots N) A \in ℂ$
33		elfzofz	$⊢ j \in (M ..^N) \to j \in (M \dots N)$
34	33	adantl	$⊢ (φ \land j \in (M ..^N)) \to j \in (M \dots N)$
35	31 32 34	rspcdva	$⊢ (φ \land j \in (M ..^N)) \to B \in ℂ$
36	2	eleq1d	$⊢ k = j + 1 \to (A \in ℂ \leftrightarrow C \in ℂ)$
37		fzofzp1	$⊢ j \in (M ..^N) \to j + 1 \in (M \dots N)$
38	37	adantl	$⊢ (φ \land j \in (M ..^N)) \to j + 1 \in (M \dots N)$
39	36 32 38	rspcdva	$⊢ (φ \land j \in (M ..^N)) \to C \in ℂ$
40	30 35 39	fsumsub	$⊢ φ \to \sum_{j \in (M ..^N)} (B - C) = \sum_{j \in (M ..^N)} B - \sum_{j \in (M ..^N)} C$
41	40	adantr	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} (B - C) = \sum_{j \in (M ..^N)} B - \sum_{j \in (M ..^N)} C$
42	1	cbvsumv	$⊢ \sum_{k \in (M ..^N)} A = \sum_{j \in (M ..^N)} B$
43		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
44	5 43	syl	$⊢ φ \to M \in ℤ$
45		eluzp1m1	$⊢ (M \in ℤ \land N \in ℤ_{\geq (M + 1)}) \to N - 1 \in ℤ_{\geq M}$
46	44 45	sylan	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to N - 1 \in ℤ_{\geq M}$
47		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
48	5 47	syl	$⊢ φ \to N \in ℤ$
49	48	adantr	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to N \in ℤ$
50		fzoval	$⊢ N \in ℤ \to (M ..^N) = (M \dots N - 1)$
51	49 50	syl	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to (M ..^N) = (M \dots N - 1)$
52		fzossfz	$⊢ (M ..^N) \subseteq (M \dots N)$
53	51 52	eqsstrrdi	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to (M \dots N - 1) \subseteq (M \dots N)$
54	53	sselda	$⊢ ((φ \land N \in ℤ_{\geq (M + 1)}) \land k \in (M \dots N - 1)) \to k \in (M \dots N)$
55	6	adantlr	$⊢ ((φ \land N \in ℤ_{\geq (M + 1)}) \land k \in (M \dots N)) \to A \in ℂ$
56	54 55	syldan	$⊢ ((φ \land N \in ℤ_{\geq (M + 1)}) \land k \in (M \dots N - 1)) \to A \in ℂ$
57	46 56 3	fsum1p	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k = M}^{N - 1} A = D + \sum_{k = M + 1}^{N - 1} A$
58	51	sumeq1d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k \in (M ..^N)} A = \sum_{k = M}^{N - 1} A$
59		fzoval	$⊢ N \in ℤ \to (M + 1 ..^N) = (M + 1 \dots N - 1)$
60	49 59	syl	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to (M + 1 ..^N) = (M + 1 \dots N - 1)$
61	60	sumeq1d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k \in (M + 1 ..^N)} A = \sum_{k = M + 1}^{N - 1} A$
62	61	oveq2d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to D + \sum_{k \in (M + 1 ..^N)} A = D + \sum_{k = M + 1}^{N - 1} A$
63	57 58 62	3eqtr4d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k \in (M ..^N)} A = D + \sum_{k \in (M + 1 ..^N)} A$
64	42 63	eqtr3id	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} B = D + \sum_{k \in (M + 1 ..^N)} A$
65		simpr	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to N \in ℤ_{\geq (M + 1)}$
66		fzp1ss	$⊢ M \in ℤ \to (M + 1 \dots N) \subseteq (M \dots N)$
67	44 66	syl	$⊢ φ \to (M + 1 \dots N) \subseteq (M \dots N)$
68	67	sselda	$⊢ (φ \land k \in (M + 1 \dots N)) \to k \in (M \dots N)$
69	68 6	syldan	$⊢ (φ \land k \in (M + 1 \dots N)) \to A \in ℂ$
70	69	adantlr	$⊢ ((φ \land N \in ℤ_{\geq (M + 1)}) \land k \in (M + 1 \dots N)) \to A \in ℂ$
71	65 70 4	fsumm1	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k = M + 1}^{N} A = \sum_{k = M + 1}^{N - 1} A + E$
72		1zzd	$⊢ φ \to 1 \in ℤ$
73	44	peano2zd	$⊢ φ \to M + 1 \in ℤ$
74	72 73 48 69 2	fsumshftm	$⊢ φ \to \sum_{k = M + 1}^{N} A = \sum_{j = M + 1 - 1}^{N - 1} C$
75	44	zcnd	$⊢ φ \to M \in ℂ$
76		ax-1cn	$⊢ 1 \in ℂ$
77		pncan	$⊢ (M \in ℂ \land 1 \in ℂ) \to M + 1 - 1 = M$
78	75 76 77	sylancl	$⊢ φ \to M + 1 - 1 = M$
79	78	oveq1d	$⊢ φ \to (M + 1 - 1 \dots N - 1) = (M \dots N - 1)$
80	48 50	syl	$⊢ φ \to (M ..^N) = (M \dots N - 1)$
81	79 80	eqtr4d	$⊢ φ \to (M + 1 - 1 \dots N - 1) = (M ..^N)$
82	81	sumeq1d	$⊢ φ \to \sum_{j = M + 1 - 1}^{N - 1} C = \sum_{j \in (M ..^N)} C$
83	74 82	eqtrd	$⊢ φ \to \sum_{k = M + 1}^{N} A = \sum_{j \in (M ..^N)} C$
84	83	adantr	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k = M + 1}^{N} A = \sum_{j \in (M ..^N)} C$
85	48 59	syl	$⊢ φ \to (M + 1 ..^N) = (M + 1 \dots N - 1)$
86	85	sumeq1d	$⊢ φ \to \sum_{k \in (M + 1 ..^N)} A = \sum_{k = M + 1}^{N - 1} A$
87	86	oveq1d	$⊢ φ \to \sum_{k \in (M + 1 ..^N)} A + E = \sum_{k = M + 1}^{N - 1} A + E$
88		fzofi	$⊢ (M + 1 ..^N) \in Fin$
89	88	a1i	$⊢ φ \to (M + 1 ..^N) \in Fin$
90		elfzofz	$⊢ k \in (M + 1 ..^N) \to k \in (M + 1 \dots N)$
91	90 69	sylan2	$⊢ (φ \land k \in (M + 1 ..^N)) \to A \in ℂ$
92	89 91	fsumcl	$⊢ φ \to \sum_{k \in (M + 1 ..^N)} A \in ℂ$
93	4	eleq1d	$⊢ k = N \to (A \in ℂ \leftrightarrow E \in ℂ)$
94		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
95	5 94	syl	$⊢ φ \to N \in (M \dots N)$
96	93 9 95	rspcdva	$⊢ φ \to E \in ℂ$
97	92 96	addcomd	$⊢ φ \to \sum_{k \in (M + 1 ..^N)} A + E = E + \sum_{k \in (M + 1 ..^N)} A$
98	87 97	eqtr3d	$⊢ φ \to \sum_{k = M + 1}^{N - 1} A + E = E + \sum_{k \in (M + 1 ..^N)} A$
99	98	adantr	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{k = M + 1}^{N - 1} A + E = E + \sum_{k \in (M + 1 ..^N)} A$
100	71 84 99	3eqtr3d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} C = E + \sum_{k \in (M + 1 ..^N)} A$
101	64 100	oveq12d	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} B - \sum_{j \in (M ..^N)} C = D + \sum_{k \in (M + 1 ..^N)} A - (E + \sum_{k \in (M + 1 ..^N)} A)$
102	12 96 92	pnpcan2d	$⊢ φ \to D + \sum_{k \in (M + 1 ..^N)} A - (E + \sum_{k \in (M + 1 ..^N)} A) = D - E$
103	102	adantr	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to D + \sum_{k \in (M + 1 ..^N)} A - (E + \sum_{k \in (M + 1 ..^N)} A) = D - E$
104	41 101 103	3eqtrd	$⊢ (φ \land N \in ℤ_{\geq (M + 1)}) \to \sum_{j \in (M ..^N)} (B - C) = D - E$
105		uzp1	$⊢ N \in ℤ_{\geq M} \to (N = M \lor N \in ℤ_{\geq (M + 1)})$
106	5 105	syl	$⊢ φ \to (N = M \lor N \in ℤ_{\geq (M + 1)})$
107	28 104 106	mpjaodan	$⊢ φ \to \sum_{j \in (M ..^N)} (B - C) = D - E$

Metamath Proof Explorer

Theorem telfsumo

Proof