Step |
Hyp |
Ref |
Expression |
1 |
|
fsumrev.1 |
|- ( ph -> K e. ZZ ) |
2 |
|
fsumrev.2 |
|- ( ph -> M e. ZZ ) |
3 |
|
fsumrev.3 |
|- ( ph -> N e. ZZ ) |
4 |
|
fsumrev.4 |
|- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC ) |
5 |
|
fsumshft.5 |
|- ( j = ( k - K ) -> A = B ) |
6 |
|
fzfid |
|- ( ph -> ( ( M + K ) ... ( N + K ) ) e. Fin ) |
7 |
1 2 3
|
mptfzshft |
|- ( ph -> ( j e. ( ( M + K ) ... ( N + K ) ) |-> ( j - K ) ) : ( ( M + K ) ... ( N + K ) ) -1-1-onto-> ( M ... N ) ) |
8 |
|
oveq1 |
|- ( j = k -> ( j - K ) = ( k - K ) ) |
9 |
|
eqid |
|- ( j e. ( ( M + K ) ... ( N + K ) ) |-> ( j - K ) ) = ( j e. ( ( M + K ) ... ( N + K ) ) |-> ( j - K ) ) |
10 |
|
ovex |
|- ( k - K ) e. _V |
11 |
8 9 10
|
fvmpt |
|- ( k e. ( ( M + K ) ... ( N + K ) ) -> ( ( j e. ( ( M + K ) ... ( N + K ) ) |-> ( j - K ) ) ` k ) = ( k - K ) ) |
12 |
11
|
adantl |
|- ( ( ph /\ k e. ( ( M + K ) ... ( N + K ) ) ) -> ( ( j e. ( ( M + K ) ... ( N + K ) ) |-> ( j - K ) ) ` k ) = ( k - K ) ) |
13 |
5 6 7 12 4
|
fsumf1o |
|- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K ) ... ( N + K ) ) B ) |