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 φjMNA
fsumshftm.5 j=k+KA=B
Assertion fsumshftm φj=MNA=k=MKNKB

Proof

Step Hyp Ref Expression
1 fsumrev.1 φK
2 fsumrev.2 φM
3 fsumrev.3 φN
4 fsumrev.4 φjMNA
5 fsumshftm.5 j=k+KA=B
6 nfcv _mA
7 nfcsb1v _jm/jA
8 csbeq1a j=mA=m/jA
9 6 7 8 cbvsumi j=MNA=m=MNm/jA
10 1 znegcld φK
11 4 ralrimiva φjMNA
12 7 nfel1 jm/jA
13 8 eleq1d j=mAm/jA
14 12 13 rspc mMNjMNAm/jA
15 11 14 mpan9 φmMNm/jA
16 csbeq1 m=kKm/jA=kK/jA
17 10 2 3 15 16 fsumshft φm=MNm/jA=k=M+KN+KkK/jA
18 2 zcnd φM
19 1 zcnd φK
20 18 19 negsubd φM+K=MK
21 3 zcnd φN
22 21 19 negsubd φN+K=NK
23 20 22 oveq12d φM+KN+K=MKNK
24 23 sumeq1d φk=M+KN+KkK/jA=k=MKNKkK/jA
25 elfzelz kMKNKk
26 25 zcnd kMKNKk
27 subneg kKkK=k+K
28 26 19 27 syl2anr φkMKNKkK=k+K
29 28 csbeq1d φkMKNKkK/jA=k+K/jA
30 ovex k+KV
31 30 5 csbie k+K/jA=B
32 29 31 eqtrdi φkMKNKkK/jA=B
33 32 sumeq2dv φk=MKNKkK/jA=k=MKNKB
34 17 24 33 3eqtrd φm=MNm/jA=k=MKNKB
35 9 34 eqtrid φj=MNA=k=MKNKB