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 ) ) |