Description: Lemma for dchrmusum and dchrisumn0 . Apply dchrisum for the function 1 / y . (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 | |
||
dchrisumn0.f | |
||
Assertion | dchrmusumlema | |