Description: Lemma for dchrvmasum . (Contributed by Mario Carneiro, 5-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rpvmasum.z | |
|
rpvmasum.l | |
||
rpvmasum.a | |
||
rpvmasum.g | |
||
rpvmasum.d | |
||
rpvmasum.1 | |
||
dchrisum.b | |
||
dchrisum.n1 | |
||
dchrvmasumif.f | |
||
dchrvmasumif.c | |
||
dchrvmasumif.s | |
||
dchrvmasumif.1 | |
||
dchrvmasumif.g | |
||
dchrvmasumif.e | |
||
dchrvmasumif.t | |
||
dchrvmasumif.2 | |
||
Assertion | dchrvmasumiflem2 | |