Metamath Proof Explorer


Theorem sumss2

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 ABkACBMBFinkAC=kBifkAC0

Proof

Step Hyp Ref Expression
1 simpll ABkACBMAB
2 iftrue mAifmAm/kC0=m/kC
3 2 adantl kACmAifmAm/kC0=m/kC
4 nfcsb1v _km/kC
5 4 nfel1 km/kC
6 csbeq1a k=mC=m/kC
7 6 eleq1d k=mCm/kC
8 5 7 rspc mAkACm/kC
9 8 impcom kACmAm/kC
10 3 9 eqeltrd kACmAifmAm/kC0
11 10 ad4ant24 ABkACBMmAifmAm/kC0
12 eldifn mBA¬mA
13 12 iffalsed mBAifmAm/kC0=0
14 13 adantl ABkACBMmBAifmAm/kC0=0
15 simpr ABkACBMBM
16 1 11 14 15 sumss ABkACBMmAifmAm/kC0=mBifmAm/kC0
17 simpll ABkACBFinAB
18 10 ad4ant24 ABkACBFinmAifmAm/kC0
19 13 adantl ABkACBFinmBAifmAm/kC0=0
20 simpr ABkACBFinBFin
21 17 18 19 20 fsumss ABkACBFinmAifmAm/kC0=mBifmAm/kC0
22 16 21 jaodan ABkACBMBFinmAifmAm/kC0=mBifmAm/kC0
23 iftrue kAifkAC0=C
24 23 sumeq2i kAifkAC0=kAC
25 nfcv _mifkAC0
26 nfv kmA
27 nfcv _k0
28 26 4 27 nfif _kifmAm/kC0
29 eleq1w k=mkAmA
30 29 6 ifbieq1d k=mifkAC0=ifmAm/kC0
31 25 28 30 cbvsumi kAifkAC0=mAifmAm/kC0
32 24 31 eqtr3i kAC=mAifmAm/kC0
33 25 28 30 cbvsumi kBifkAC0=mBifmAm/kC0
34 22 32 33 3eqtr4g ABkACBMBFinkAC=kBifkAC0