Description: Lemma for dchrisum0 . (Contributed by Mario Carneiro, 12-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rpvmasum.z | |
|
rpvmasum.l | |
||
rpvmasum.a | |
||
rpvmasum2.g | |
||
rpvmasum2.d | |
||
rpvmasum2.1 | |
||
rpvmasum2.w | |
||
dchrisum0.b | |
||
dchrisum0lem1.f | |
||
dchrisum0.c | |
||
dchrisum0.s | |
||
dchrisum0.1 | |
||
dchrisum0lem2.h | |
||
dchrisum0lem2.u | |
||
Assertion | dchrisum0lem2a | |