Description: Lemma for ramub1 . (Contributed by Mario Carneiro, 23-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ramub1.m | |
|
ramub1.r | |
||
ramub1.f | |
||
ramub1.g | |
||
ramub1.1 | |
||
ramub1.2 | |
||
ramub1.3 | |
||
ramub1.4 | |
||
ramub1.5 | |
||
ramub1.6 | |
||
ramub1.x | |
||
ramub1.h | |
||
ramub1.d | |
||
ramub1.w | |
||
ramub1.7 | |
||
ramub1.8 | |
||
ramub1.e | |
||
ramub1.v | |
||
ramub1.9 | |
||
ramub1.s | |
||
Assertion | ramub1lem1 | |