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 ⊢ ( 𝑘 = 𝑗 → 𝐴 = 𝐵 )
telfsum.2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → 𝐴 = 𝐶 )
telfsum.3 ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐷 )
telfsum.4 ⊢ ( 𝑘 = ( 𝑁 + 1 ) → 𝐴 = 𝐸 )
telfsum.5 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
telfsum.6 ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
telfsum.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ ℂ )
Assertion telfsum2 ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ( 𝐶 − 𝐵 ) = ( 𝐸 − 𝐷 ) )

Proof

Step Hyp Ref Expression
1 telfsum.1 ⊢ ( 𝑘 = 𝑗 → 𝐴 = 𝐵 )
2 telfsum.2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → 𝐴 = 𝐶 )
3 telfsum.3 ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐷 )
4 telfsum.4 ⊢ ( 𝑘 = ( 𝑁 + 1 ) → 𝐴 = 𝐸 )
5 telfsum.5 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
6 telfsum.6 ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
7 telfsum.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ ℂ )
8 fzval3 ⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ... 𝑁 ) = ( 𝑀 ..^ ( 𝑁 + 1 ) ) )
9 5 8 syl ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) = ( 𝑀 ..^ ( 𝑁 + 1 ) ) )
10 9 sumeq1d ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ( 𝐶 − 𝐵 ) = Σ 𝑗 ∈ ( 𝑀 ..^ ( 𝑁 + 1 ) ) ( 𝐶 − 𝐵 ) )
11 1 2 3 4 6 7 telfsumo2 ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ ( 𝑁 + 1 ) ) ( 𝐶 − 𝐵 ) = ( 𝐸 − 𝐷 ) )
12 10 11 eqtrd ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ( 𝐶 − 𝐵 ) = ( 𝐸 − 𝐷 ) )