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 φ K
fsumrev.2 φ M
fsumrev.3 φ N
fsumrev.4 φ j M N A
fsumshftm.5 j = k + K A = B
Assertion fsumshftm φ j = M N A = k = M K N K B

Proof

Step Hyp Ref Expression
1 fsumrev.1 φ K
2 fsumrev.2 φ M
3 fsumrev.3 φ N
4 fsumrev.4 φ j M N A
5 fsumshftm.5 j = k + K A = B
6 nfcv _ m A
7 nfcsb1v _ j m / j A
8 csbeq1a j = m A = m / j A
9 6 7 8 cbvsumi j = M N A = m = M N m / j A
10 1 znegcld φ K
11 4 ralrimiva φ j M N A
12 7 nfel1 j m / j A
13 8 eleq1d j = m A m / j A
14 12 13 rspc m M N j M N A m / j A
15 11 14 mpan9 φ m M N m / j A
16 csbeq1 m = k K m / j A = k K / j A
17 10 2 3 15 16 fsumshft φ m = M N m / j A = k = M + K N + K k K / j A
18 2 zcnd φ M
19 1 zcnd φ K
20 18 19 negsubd φ M + K = M K
21 3 zcnd φ N
22 21 19 negsubd φ N + K = N K
23 20 22 oveq12d φ M + K N + K = M K N K
24 23 sumeq1d φ k = M + K N + K k K / j A = k = M K N K k K / j A
25 elfzelz k M K N K k
26 25 zcnd k M K N K k
27 subneg k K k K = k + K
28 26 19 27 syl2anr φ k M K N K k K = k + K
29 28 csbeq1d φ k M K N K k K / j A = k + K / j A
30 ovex k + K V
31 30 5 csbie k + K / j A = B
32 29 31 syl6eq φ k M K N K k K / j A = B
33 32 sumeq2dv φ k = M K N K k K / j A = k = M K N K B
34 17 24 33 3eqtrd φ m = M N m / j A = k = M K N K B
35 9 34 syl5eq φ j = M N A = k = M K N K B