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..^NC−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…NA∈ℂ
14 elfzofz ⊢j∈M..^N→j∈M…N
15 1 eleq1d ⊢k=j→A∈ℂ↔B∈ℂ
16 15 rspccva ⊢∀k∈M…NA∈ℂ∧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…NA∈ℂ∧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..^NC−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..^NC−B=E−D