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