Theorem telfsum

Description: Sum of a telescoping series. (Contributed by Scott Fenton, 24-Apr-2014) (Revised by Mario Carneiro, 2-May-2016)

	Ref	Expression
Hypotheses	telfsum.1	$$⊢k=j\to A=B$$
	telfsum.2	$$⊢k=j+1\to A=C$$
	telfsum.3	$$⊢k=M\to A=D$$
	telfsum.4	$$⊢k=N+1\to A=E$$
	telfsum.5	$$⊢\phi \to N\in \mathbb{Z}$$
	telfsum.6	$$⊢\phi \to N+1\in {\mathbb{Z}}_{\ge M}$$
	telfsum.7	$$⊢\left(\phi \wedge k\in \left(M\dots N+1\right)\right)\to A\in ℂ$$
Assertion	telfsum	$$⊢\phi \to \sum _{j=M}^N\left(B-C\right)=D-E$$

Proof

Step	Hyp	Ref	Expression
1		telfsum.1	$$⊢k=j\to A=B$$
2		telfsum.2	$$⊢k=j+1\to A=C$$
3		telfsum.3	$$⊢k=M\to A=D$$
4		telfsum.4	$$⊢k=N+1\to A=E$$
5		telfsum.5	$$⊢\phi \to N\in \mathbb{Z}$$
6		telfsum.6	$$⊢\phi \to N+1\in {\mathbb{Z}}_{\ge M}$$
7		telfsum.7	$$⊢\left(\phi \wedge k\in \left(M\dots N+1\right)\right)\to A\in ℂ$$
8		fzval3	$$⊢N\in \mathbb{Z}\to \left(M\dots N\right)=\left(M..^N+1\right)$$
9	5 8	syl	$$⊢\phi \to \left(M\dots N\right)=\left(M..^N+1\right)$$
10	9	sumeq1d	$$⊢\phi \to \sum _{j=M}^N\left(B-C\right)=\sum _{j\in \left(M..^N+1\right)}\left(B-C\right)$$
11	1 2 3 4 6 7	telfsumo	$$⊢\phi \to \sum _{j\in \left(M..^N+1\right)}\left(B-C\right)=D-E$$
12	10 11	eqtrd	$$⊢\phi \to \sum _{j=M}^N\left(B-C\right)=D-E$$