Metamath Proof Explorer
Description: The product of two positive surreals is positive. Theorem 9 of Conway
p. 20. (Contributed by Scott Fenton, 6-Mar-2025)
|
|
Ref |
Expression |
|
Hypotheses |
mulsgt0d.1 |
|
|
|
mulsgt0d.2 |
|
|
|
mulsgt0d.3 |
|
|
|
mulsgt0d.4 |
|
|
Assertion |
mulsgt0d |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
mulsgt0d.1 |
|
2 |
|
mulsgt0d.2 |
|
3 |
|
mulsgt0d.3 |
|
4 |
|
mulsgt0d.4 |
|
5 |
|
mulsgt0 |
|
6 |
1 3 2 4 5
|
syl22anc |
|