Step |
Hyp |
Ref |
Expression |
1 |
|
telfsum.1 |
|- ( k = j -> A = B ) |
2 |
|
telfsum.2 |
|- ( k = ( j + 1 ) -> A = C ) |
3 |
|
telfsum.3 |
|- ( k = M -> A = D ) |
4 |
|
telfsum.4 |
|- ( k = ( N + 1 ) -> A = E ) |
5 |
|
telfsum.5 |
|- ( ph -> N e. ZZ ) |
6 |
|
telfsum.6 |
|- ( ph -> ( N + 1 ) e. ( ZZ>= ` M ) ) |
7 |
|
telfsum.7 |
|- ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC ) |
8 |
|
fzval3 |
|- ( N e. ZZ -> ( M ... N ) = ( M ..^ ( N + 1 ) ) ) |
9 |
5 8
|
syl |
|- ( ph -> ( M ... N ) = ( M ..^ ( N + 1 ) ) ) |
10 |
9
|
sumeq1d |
|- ( ph -> sum_ j e. ( M ... N ) ( B - C ) = sum_ j e. ( M ..^ ( N + 1 ) ) ( B - C ) ) |
11 |
1 2 3 4 6 7
|
telfsumo |
|- ( ph -> sum_ j e. ( M ..^ ( N + 1 ) ) ( B - C ) = ( D - E ) ) |
12 |
10 11
|
eqtrd |
|- ( ph -> sum_ j e. ( M ... N ) ( B - C ) = ( D - E ) ) |