This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem telfsum2

Description: Sum of a telescoping series. (Contributed by Mario Carneiro, 15-Jun-2014) (Revised by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses telfsum.1 ⊢ k = j → A = B
telfsum.2 ⊢ k = j + 1 → A = C
telfsum.3 ⊢ k = M → A = D
telfsum.4 ⊢ k = N + 1 → A = E
telfsum.5 ⊢ φ → N ∈ ℤ
telfsum.6 ⊢ φ → N + 1 ∈ ℤ ≥ M
telfsum.7 ⊢ φ ∧ k ∈ M … N + 1 → A ∈ ℂ
Assertion telfsum2 ⊢ φ → ∑ j = M N C − B = E − D

Proof

Step Hyp Ref Expression
1 telfsum.1 ⊢ k = j → A = B
2 telfsum.2 ⊢ k = j + 1 → A = C
3 telfsum.3 ⊢ k = M → A = D
4 telfsum.4 ⊢ k = N + 1 → A = E
5 telfsum.5 ⊢ φ → N ∈ ℤ
6 telfsum.6 ⊢ φ → N + 1 ∈ ℤ ≥ M
7 telfsum.7 ⊢ φ ∧ k ∈ M … N + 1 → A ∈ ℂ
8 fzval3 ⊢ N ∈ ℤ → M … N = M ..^ N + 1
9 5 8 syl ⊢ φ → M … N = M ..^ N + 1
10 9 sumeq1d ⊢ φ → ∑ j = M N C − B = ∑ j ∈ M ..^ N + 1 C − B
11 1 2 3 4 6 7 telfsumo2 ⊢ φ → ∑ j ∈ M ..^ N + 1 C − B = E − D
12 10 11 eqtrd ⊢ φ → ∑ j = M N C − B = E − D