Metamath Proof Explorer


Theorem mulsgt0d

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 φ A No
mulsgt0d.2 φ B No
mulsgt0d.3 φ 0 s < s A
mulsgt0d.4 φ 0 s < s B
Assertion mulsgt0d φ 0 s < s A s B

Proof

Step Hyp Ref Expression
1 mulsgt0d.1 φ A No
2 mulsgt0d.2 φ B No
3 mulsgt0d.3 φ 0 s < s A
4 mulsgt0d.4 φ 0 s < s B
5 mulsgt0 A No 0 s < s A B No 0 s < s B 0 s < s A s B
6 1 3 2 4 5 syl22anc φ 0 s < s A s B