Metamath Proof Explorer

Theorem telfsumo2

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

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

Proof

Step Hyp Ref Expression
1 telfsumo.1 ⊢ k = j → A = B
2 telfsumo.2 ⊢ k = j + 1 → A = C
3 telfsumo.3 ⊢ k = M → A = D
4 telfsumo.4 ⊢ k = N → A = E
5 telfsumo.5 ⊢ φ → N ∈ ℤ ≥ M
6 telfsumo.6 ⊢ φ ∧ k ∈ M … N → A ∈ ℂ
7 1 negeqd ⊢ k = j → − A = − B
8 2 negeqd ⊢ k = j + 1 → − A = − C
9 3 negeqd ⊢ k = M → − A = − D
10 4 negeqd ⊢ k = N → − A = − E
11 6 negcld ⊢ φ ∧ k ∈ M … N → − A ∈ ℂ
12 7 8 9 10 5 11 telfsumo ⊢ φ → ∑ j ∈ M ..^ N - B - − C = - D - − E
13 6 ralrimiva ⊢ φ → ∀ k ∈ M … N A ∈ ℂ
14 elfzofz ⊢ j ∈ M ..^ N → j ∈ M … N
15 1 eleq1d ⊢ k = j → A ∈ ℂ ↔ B ∈ ℂ
16 15 rspccva ⊢ ∀ k ∈ M … N A ∈ ℂ ∧ j ∈ M … N → B ∈ ℂ
17 13 14 16 syl2an ⊢ φ ∧ j ∈ M ..^ N → B ∈ ℂ
18 fzofzp1 ⊢ j ∈ M ..^ N → j + 1 ∈ M … N
19 2 eleq1d ⊢ k = j + 1 → A ∈ ℂ ↔ C ∈ ℂ
20 19 rspccva ⊢ ∀ k ∈ M … N A ∈ ℂ ∧ j + 1 ∈ M … N → C ∈ ℂ
21 13 18 20 syl2an ⊢ φ ∧ j ∈ M ..^ N → C ∈ ℂ
22 17 21 neg2subd ⊢ φ ∧ j ∈ M ..^ N → - B - − C = C − B
23 22 sumeq2dv ⊢ φ → ∑ j ∈ M ..^ N - B - − C = ∑ j ∈ M ..^ N C − B
24 3 eleq1d ⊢ k = M → A ∈ ℂ ↔ D ∈ ℂ
25 eluzfz1 ⊢ N ∈ ℤ ≥ M → M ∈ M … N
26 5 25 syl ⊢ φ → M ∈ M … N
27 24 13 26 rspcdva ⊢ φ → D ∈ ℂ
28 4 eleq1d ⊢ k = N → A ∈ ℂ ↔ E ∈ ℂ
29 eluzfz2 ⊢ N ∈ ℤ ≥ M → N ∈ M … N
30 5 29 syl ⊢ φ → N ∈ M … N
31 28 13 30 rspcdva ⊢ φ → E ∈ ℂ
32 27 31 neg2subd ⊢ φ → - D - − E = E − D
33 12 23 32 3eqtr3d ⊢ φ → ∑ j ∈ M ..^ N C − B = E − D