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 e. No /\ B e. No ) -> ( A x.s B ) e. No )

Proof

Step Hyp Ref Expression
1 0sno 
 |-  0s e. No
2 1 1 pm3.2i 
 |-  ( 0s e. No /\ 0s e. No )
3 mulsprop 
 |-  ( ( ( A e. No /\ B e. No ) /\ ( 0s e. No /\ 0s e. No ) /\ ( 0s e. No /\ 0s e. No ) ) -> ( ( A x.s B ) e. No /\ ( ( 0s  ( ( 0s x.s 0s ) -s ( 0s x.s 0s ) )
4 2 2 3 mp3an23 
 |-  ( ( A e. No /\ B e. No ) -> ( ( A x.s B ) e. No /\ ( ( 0s  ( ( 0s x.s 0s ) -s ( 0s x.s 0s ) )
5 4 simpld 
 |-  ( ( A e. No /\ B e. No ) -> ( A x.s B ) e. No )