| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fzosumm1.1 |
|- ( ph -> ( N - 1 ) e. ( ZZ>= ` M ) ) |
| 2 |
|
fzosumm1.2 |
|- ( ( ph /\ k e. ( M ..^ N ) ) -> A e. CC ) |
| 3 |
|
fzosumm1.3 |
|- ( k = ( N - 1 ) -> A = B ) |
| 4 |
|
fzosumm1.n |
|- ( ph -> N e. ZZ ) |
| 5 |
|
fzoval |
|- ( N e. ZZ -> ( M ..^ N ) = ( M ... ( N - 1 ) ) ) |
| 6 |
4 5
|
syl |
|- ( ph -> ( M ..^ N ) = ( M ... ( N - 1 ) ) ) |
| 7 |
6
|
eqcomd |
|- ( ph -> ( M ... ( N - 1 ) ) = ( M ..^ N ) ) |
| 8 |
7
|
eleq2d |
|- ( ph -> ( k e. ( M ... ( N - 1 ) ) <-> k e. ( M ..^ N ) ) ) |
| 9 |
8
|
biimpa |
|- ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> k e. ( M ..^ N ) ) |
| 10 |
9 2
|
syldan |
|- ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> A e. CC ) |
| 11 |
1 10 3
|
fsumm1 |
|- ( ph -> sum_ k e. ( M ... ( N - 1 ) ) A = ( sum_ k e. ( M ... ( ( N - 1 ) - 1 ) ) A + B ) ) |
| 12 |
6
|
sumeq1d |
|- ( ph -> sum_ k e. ( M ..^ N ) A = sum_ k e. ( M ... ( N - 1 ) ) A ) |
| 13 |
|
eluzelz |
|- ( ( N - 1 ) e. ( ZZ>= ` M ) -> ( N - 1 ) e. ZZ ) |
| 14 |
|
fzoval |
|- ( ( N - 1 ) e. ZZ -> ( M ..^ ( N - 1 ) ) = ( M ... ( ( N - 1 ) - 1 ) ) ) |
| 15 |
1 13 14
|
3syl |
|- ( ph -> ( M ..^ ( N - 1 ) ) = ( M ... ( ( N - 1 ) - 1 ) ) ) |
| 16 |
15
|
sumeq1d |
|- ( ph -> sum_ k e. ( M ..^ ( N - 1 ) ) A = sum_ k e. ( M ... ( ( N - 1 ) - 1 ) ) A ) |
| 17 |
16
|
oveq1d |
|- ( ph -> ( sum_ k e. ( M ..^ ( N - 1 ) ) A + B ) = ( sum_ k e. ( M ... ( ( N - 1 ) - 1 ) ) A + B ) ) |
| 18 |
11 12 17
|
3eqtr4d |
|- ( ph -> sum_ k e. ( M ..^ N ) A = ( sum_ k e. ( M ..^ ( N - 1 ) ) A + B ) ) |