Metamath Proof Explorer


Theorem telfsum

Description: Sum of a telescoping series. (Contributed by Scott Fenton, 24-Apr-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 telfsum ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ( 𝐵𝐶 ) = ( 𝐷𝐸 ) )

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 telfsumo ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ ( 𝑁 + 1 ) ) ( 𝐵𝐶 ) = ( 𝐷𝐸 ) )
12 10 11 eqtrd ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ( 𝐵𝐶 ) = ( 𝐷𝐸 ) )