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 | |
|
fsumrev.2 | |
||
fsumrev.3 | |
||
fsumrev.4 | |
||
fsumshftm.5 | |
||
Assertion | fsumshftm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fsumrev.1 | |
|
2 | fsumrev.2 | |
|
3 | fsumrev.3 | |
|
4 | fsumrev.4 | |
|
5 | fsumshftm.5 | |
|
6 | nfcv | |
|
7 | nfcsb1v | |
|
8 | csbeq1a | |
|
9 | 6 7 8 | cbvsumi | |
10 | 1 | znegcld | |
11 | 4 | ralrimiva | |
12 | 7 | nfel1 | |
13 | 8 | eleq1d | |
14 | 12 13 | rspc | |
15 | 11 14 | mpan9 | |
16 | csbeq1 | |
|
17 | 10 2 3 15 16 | fsumshft | |
18 | 2 | zcnd | |
19 | 1 | zcnd | |
20 | 18 19 | negsubd | |
21 | 3 | zcnd | |
22 | 21 19 | negsubd | |
23 | 20 22 | oveq12d | |
24 | 23 | sumeq1d | |
25 | elfzelz | |
|
26 | 25 | zcnd | |
27 | subneg | |
|
28 | 26 19 27 | syl2anr | |
29 | 28 | csbeq1d | |
30 | ovex | |
|
31 | 30 5 | csbie | |
32 | 29 31 | eqtrdi | |
33 | 32 | sumeq2dv | |
34 | 17 24 33 | 3eqtrd | |
35 | 9 34 | eqtrid | |