Description: Lemma for surreal multiplication. Finally, we remove the restriction on E and F from mulsproplem12 and mulsproplem13 . This completes the induction on surreal multiplication. mulsprop brings all this together technically. (Contributed by Scott Fenton, 5-Mar-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mulsproplem.1 | |
|
mulsproplem.2 | |
||
mulsproplem.3 | |
||
mulsproplem.4 | |
||
mulsproplem.5 | |
||
mulsproplem.6 | |
||
mulsproplem.7 | |
||
Assertion | mulsproplem14 | |