Metamath Proof Explorer


Theorem mulscl

Description: The surreals are closed under multiplication. Theorem 8(i) of Conway p. 19. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Assertion mulscl A No B No A s B No

Proof

Step Hyp Ref Expression
1 0sno 0 s No
2 1 1 pm3.2i 0 s No 0 s No
3 mulsprop A No B No 0 s No 0 s No 0 s No 0 s No A s B No 0 s < s 0 s 0 s < s 0 s 0 s s 0 s - s 0 s s 0 s < s 0 s s 0 s - s 0 s s 0 s
4 2 2 3 mp3an23 A No B No A s B No 0 s < s 0 s 0 s < s 0 s 0 s s 0 s - s 0 s s 0 s < s 0 s s 0 s - s 0 s s 0 s
5 4 simpld A No B No A s B No