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 ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐶𝐵 ) = ( 𝐸𝐷 ) )