Description: Change the index set to a subset by adding zeroes. (Contributed by Thierry Arnoux, 19-Jun-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | esumss.p | |
|
esumss.a | |
||
esumss.b | |
||
esumss.1 | |
||
esumss.2 | |
||
esumss.3 | |
||
esumss.4 | |
||
Assertion | esumss | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | esumss.p | |
|
2 | esumss.a | |
|
3 | esumss.b | |
|
4 | esumss.1 | |
|
5 | esumss.2 | |
|
6 | esumss.3 | |
|
7 | esumss.4 | |
|
8 | 3 2 | resmptf | |
9 | 4 8 | syl | |
10 | 9 | oveq2d | |
11 | xrge0base | |
|
12 | xrge00 | |
|
13 | xrge0cmn | |
|
14 | 13 | a1i | |
15 | xrge0tps | |
|
16 | 15 | a1i | |
17 | nfcv | |
|
18 | eqid | |
|
19 | 1 3 17 6 18 | fmptdF | |
20 | 1 3 2 7 5 | suppss2f | |
21 | 11 12 14 16 5 19 20 | tsmsres | |
22 | 10 21 | eqtr3d | |
23 | 22 | unieqd | |
24 | df-esum | |
|
25 | df-esum | |
|
26 | 23 24 25 | 3eqtr4g | |