Step |
Hyp |
Ref |
Expression |
1 |
|
fsumshftd.1 |
|- ( ph -> K e. ZZ ) |
2 |
|
fsumshftd.2 |
|- ( ph -> M e. ZZ ) |
3 |
|
fsumshftd.3 |
|- ( ph -> N e. ZZ ) |
4 |
|
fsumshftd.4 |
|- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC ) |
5 |
|
fsumshftd.5 |
|- ( ( ph /\ j = ( k - K ) ) -> A = B ) |
6 |
|
nfcv |
|- F/_ w A |
7 |
|
nfcsb1v |
|- F/_ j [_ w / j ]_ A |
8 |
|
csbeq1a |
|- ( j = w -> A = [_ w / j ]_ A ) |
9 |
6 7 8
|
cbvsumi |
|- sum_ j e. ( M ... N ) A = sum_ w e. ( M ... N ) [_ w / j ]_ A |
10 |
|
nfv |
|- F/ j ( ph /\ w e. ( M ... N ) ) |
11 |
7
|
nfel1 |
|- F/ j [_ w / j ]_ A e. CC |
12 |
10 11
|
nfim |
|- F/ j ( ( ph /\ w e. ( M ... N ) ) -> [_ w / j ]_ A e. CC ) |
13 |
|
eleq1w |
|- ( j = w -> ( j e. ( M ... N ) <-> w e. ( M ... N ) ) ) |
14 |
13
|
anbi2d |
|- ( j = w -> ( ( ph /\ j e. ( M ... N ) ) <-> ( ph /\ w e. ( M ... N ) ) ) ) |
15 |
8
|
eleq1d |
|- ( j = w -> ( A e. CC <-> [_ w / j ]_ A e. CC ) ) |
16 |
14 15
|
imbi12d |
|- ( j = w -> ( ( ( ph /\ j e. ( M ... N ) ) -> A e. CC ) <-> ( ( ph /\ w e. ( M ... N ) ) -> [_ w / j ]_ A e. CC ) ) ) |
17 |
12 16 4
|
chvarfv |
|- ( ( ph /\ w e. ( M ... N ) ) -> [_ w / j ]_ A e. CC ) |
18 |
|
csbeq1 |
|- ( w = ( k - K ) -> [_ w / j ]_ A = [_ ( k - K ) / j ]_ A ) |
19 |
1 2 3 17 18
|
fsumshft |
|- ( ph -> sum_ w e. ( M ... N ) [_ w / j ]_ A = sum_ k e. ( ( M + K ) ... ( N + K ) ) [_ ( k - K ) / j ]_ A ) |
20 |
|
ovexd |
|- ( ph -> ( k - K ) e. _V ) |
21 |
20 5
|
csbied |
|- ( ph -> [_ ( k - K ) / j ]_ A = B ) |
22 |
21
|
sumeq2sdv |
|- ( ph -> sum_ k e. ( ( M + K ) ... ( N + K ) ) [_ ( k - K ) / j ]_ A = sum_ k e. ( ( M + K ) ... ( N + K ) ) B ) |
23 |
19 22
|
eqtrd |
|- ( ph -> sum_ w e. ( M ... N ) [_ w / j ]_ A = sum_ k e. ( ( M + K ) ... ( N + K ) ) B ) |
24 |
9 23
|
syl5eq |
|- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M + K ) ... ( N + K ) ) B ) |