Description: Change the index set of a sum by adding zeroes. (Contributed by Mario Carneiro, 15-Jul-2013) (Revised by Mario Carneiro, 20-Apr-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | sumss2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpll | |
|
2 | iftrue | |
|
3 | 2 | adantl | |
4 | nfcsb1v | |
|
5 | 4 | nfel1 | |
6 | csbeq1a | |
|
7 | 6 | eleq1d | |
8 | 5 7 | rspc | |
9 | 8 | impcom | |
10 | 3 9 | eqeltrd | |
11 | 10 | ad4ant24 | |
12 | eldifn | |
|
13 | 12 | iffalsed | |
14 | 13 | adantl | |
15 | simpr | |
|
16 | 1 11 14 15 | sumss | |
17 | simpll | |
|
18 | 10 | ad4ant24 | |
19 | 13 | adantl | |
20 | simpr | |
|
21 | 17 18 19 20 | fsumss | |
22 | 16 21 | jaodan | |
23 | iftrue | |
|
24 | 23 | sumeq2i | |
25 | nfcv | |
|
26 | nfv | |
|
27 | nfcv | |
|
28 | 26 4 27 | nfif | |
29 | eleq1w | |
|
30 | 29 6 | ifbieq1d | |
31 | 25 28 30 | cbvsumi | |
32 | 24 31 | eqtr3i | |
33 | 25 28 30 | cbvsumi | |
34 | 22 32 33 | 3eqtr4g | |