Metamath Proof Explorer

Theorem fsumshftm

Description: Negative index shift of a finite sum. (Contributed by NM, 28-Nov-2005) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsumrev.1 
|- ( ph -> K e. ZZ )
fsumrev.2 
|- ( ph -> M e. ZZ )
fsumrev.3 
|- ( ph -> N e. ZZ )
fsumrev.4 
|- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )
fsumshftm.5 
|- ( j = ( k + K ) -> A = B )
Assertion fsumshftm 
|- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M - K ) ... ( N - K ) ) B )

Proof

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 fsumshftm.5 
 |-  ( j = ( k + K ) -> A = B )
6 nfcv 
 |-  F/_ m A
7 nfcsb1v 
 |-  F/_ j [_ m / j ]_ A
8 csbeq1a 
 |-  ( j = m -> A = [_ m / j ]_ A )
9 6 7 8 cbvsumi 
 |-  sum_ j e. ( M ... N ) A = sum_ m e. ( M ... N ) [_ m / j ]_ A
10 1 znegcld 
 |-  ( ph -> -u K e. ZZ )
11 4 ralrimiva 
 |-  ( ph -> A. j e. ( M ... N ) A e. CC )
12 7 nfel1 
 |-  F/ j [_ m / j ]_ A e. CC
13 8 eleq1d 
 |-  ( j = m -> ( A e. CC <-> [_ m / j ]_ A e. CC ) )
14 12 13 rspc 
 |-  ( m e. ( M ... N ) -> ( A. j e. ( M ... N ) A e. CC -> [_ m / j ]_ A e. CC ) )
15 11 14 mpan9 
 |-  ( ( ph /\ m e. ( M ... N ) ) -> [_ m / j ]_ A e. CC )
16 csbeq1 
 |-  ( m = ( k - -u K ) -> [_ m / j ]_ A = [_ ( k - -u K ) / j ]_ A )
17 10 2 3 15 16 fsumshft 
 |-  ( ph -> sum_ m e. ( M ... N ) [_ m / j ]_ A = sum_ k e. ( ( M + -u K ) ... ( N + -u K ) ) [_ ( k - -u K ) / j ]_ A )
18 2 zcnd 
 |-  ( ph -> M e. CC )
19 1 zcnd 
 |-  ( ph -> K e. CC )
20 18 19 negsubd 
 |-  ( ph -> ( M + -u K ) = ( M - K ) )
21 3 zcnd 
 |-  ( ph -> N e. CC )
22 21 19 negsubd 
 |-  ( ph -> ( N + -u K ) = ( N - K ) )
23 20 22 oveq12d 
 |-  ( ph -> ( ( M + -u K ) ... ( N + -u K ) ) = ( ( M - K ) ... ( N - K ) ) )
24 23 sumeq1d 
 |-  ( ph -> sum_ k e. ( ( M + -u K ) ... ( N + -u K ) ) [_ ( k - -u K ) / j ]_ A = sum_ k e. ( ( M - K ) ... ( N - K ) ) [_ ( k - -u K ) / j ]_ A )
25 elfzelz 
 |-  ( k e. ( ( M - K ) ... ( N - K ) ) -> k e. ZZ )
26 25 zcnd 
 |-  ( k e. ( ( M - K ) ... ( N - K ) ) -> k e. CC )
27 subneg 
 |-  ( ( k e. CC /\ K e. CC ) -> ( k - -u K ) = ( k + K ) )
28 26 19 27 syl2anr 
 |-  ( ( ph /\ k e. ( ( M - K ) ... ( N - K ) ) ) -> ( k - -u K ) = ( k + K ) )
29 28 csbeq1d 
 |-  ( ( ph /\ k e. ( ( M - K ) ... ( N - K ) ) ) -> [_ ( k - -u K ) / j ]_ A = [_ ( k + K ) / j ]_ A )
30 ovex 
 |-  ( k + K ) e. _V
31 30 5 csbie 
 |-  [_ ( k + K ) / j ]_ A = B
32 29 31 eqtrdi 
 |-  ( ( ph /\ k e. ( ( M - K ) ... ( N - K ) ) ) -> [_ ( k - -u K ) / j ]_ A = B )
33 32 sumeq2dv 
 |-  ( ph -> sum_ k e. ( ( M - K ) ... ( N - K ) ) [_ ( k - -u K ) / j ]_ A = sum_ k e. ( ( M - K ) ... ( N - K ) ) B )
34 17 24 33 3eqtrd 
 |-  ( ph -> sum_ m e. ( M ... N ) [_ m / j ]_ A = sum_ k e. ( ( M - K ) ... ( N - K ) ) B )
35 9 34 eqtrid 
 |-  ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( M - K ) ... ( N - K ) ) B )