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

Metamath Proof Explorer

Theorem telfsumo2

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

Ref Expression
Hypotheses telfsumo.1 ⊢ ( 𝑘 = 𝑗 → 𝐴 = 𝐵 )
telfsumo.2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → 𝐴 = 𝐶 )
telfsumo.3 ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐷 )
telfsumo.4 ⊢ ( 𝑘 = 𝑁 → 𝐴 = 𝐸 )
telfsumo.5 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
telfsumo.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
Assertion telfsumo2 ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐶 − 𝐵 ) = ( 𝐸 − 𝐷 ) )

Proof

Step Hyp Ref Expression
1 telfsumo.1 ⊢ ( 𝑘 = 𝑗 → 𝐴 = 𝐵 )
2 telfsumo.2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → 𝐴 = 𝐶 )
3 telfsumo.3 ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐷 )
4 telfsumo.4 ⊢ ( 𝑘 = 𝑁 → 𝐴 = 𝐸 )
5 telfsumo.5 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
6 telfsumo.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
7 1 negeqd ⊢ ( 𝑘 = 𝑗 → - 𝐴 = - 𝐵 )
8 2 negeqd ⊢ ( 𝑘 = ( 𝑗 + 1 ) → - 𝐴 = - 𝐶 )
9 3 negeqd ⊢ ( 𝑘 = 𝑀 → - 𝐴 = - 𝐷 )
10 4 negeqd ⊢ ( 𝑘 = 𝑁 → - 𝐴 = - 𝐸 )
11 6 negcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → - 𝐴 ∈ ℂ )
12 7 8 9 10 5 11 telfsumo ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( - 𝐵 − - 𝐶 ) = ( - 𝐷 − - 𝐸 ) )
13 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ )
14 elfzofz ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑗 ∈ ( 𝑀 ... 𝑁 ) )
15 1 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐴 ∈ ℂ ↔ 𝐵 ∈ ℂ ) )
16 15 rspccva ⊢ ( ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐵 ∈ ℂ )
17 13 14 16 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐵 ∈ ℂ )
18 fzofzp1 ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑗 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
19 2 eleq1d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝐴 ∈ ℂ ↔ 𝐶 ∈ ℂ ) )
20 19 rspccva ⊢ ( ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ ∧ ( 𝑗 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝐶 ∈ ℂ )
21 13 18 20 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐶 ∈ ℂ )
22 17 21 neg2subd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( - 𝐵 − - 𝐶 ) = ( 𝐶 − 𝐵 ) )
23 22 sumeq2dv ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( - 𝐵 − - 𝐶 ) = Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐶 − 𝐵 ) )
24 3 eleq1d ⊢ ( 𝑘 = 𝑀 → ( 𝐴 ∈ ℂ ↔ 𝐷 ∈ ℂ ) )
25 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
26 5 25 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
27 24 13 26 rspcdva ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
28 4 eleq1d ⊢ ( 𝑘 = 𝑁 → ( 𝐴 ∈ ℂ ↔ 𝐸 ∈ ℂ ) )
29 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
30 5 29 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
31 28 13 30 rspcdva ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
32 27 31 neg2subd ⊢ ( 𝜑 → ( - 𝐷 − - 𝐸 ) = ( 𝐸 − 𝐷 ) )
33 12 23 32 3eqtr3d ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐶 − 𝐵 ) = ( 𝐸 − 𝐷 ) )