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	⊢ ( 𝑘 = 𝑗 → 𝐴 = 𝐵 )
	telfsum.2	⊢ ( 𝑘 = ( 𝑗 + 1 ) → 𝐴 = 𝐶 )
	telfsum.3	⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐷 )
	telfsum.4	⊢ ( 𝑘 = ( 𝑁 + 1 ) → 𝐴 = 𝐸 )
	telfsum.5	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	telfsum.6	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
	telfsum.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ ℂ )
Assertion	telfsum	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ( 𝐵 − 𝐶 ) = ( 𝐷 − 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		telfsum.1	⊢ ( 𝑘 = 𝑗 → 𝐴 = 𝐵 )
2		telfsum.2	⊢ ( 𝑘 = ( 𝑗 + 1 ) → 𝐴 = 𝐶 )
3		telfsum.3	⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐷 )
4		telfsum.4	⊢ ( 𝑘 = ( 𝑁 + 1 ) → 𝐴 = 𝐸 )
5		telfsum.5	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
6		telfsum.6	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
7		telfsum.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ ℂ )
8		fzval3	⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ... 𝑁 ) = ( 𝑀 ..^ ( 𝑁 + 1 ) ) )
9	5 8	syl	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) = ( 𝑀 ..^ ( 𝑁 + 1 ) ) )
10	9	sumeq1d	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ( 𝐵 − 𝐶 ) = Σ 𝑗 ∈ ( 𝑀 ..^ ( 𝑁 + 1 ) ) ( 𝐵 − 𝐶 ) )
11	1 2 3 4 6 7	telfsumo	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ ( 𝑁 + 1 ) ) ( 𝐵 − 𝐶 ) = ( 𝐷 − 𝐸 ) )
12	10 11	eqtrd	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ( 𝐵 − 𝐶 ) = ( 𝐷 − 𝐸 ) )