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	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ·s 𝐵 ) ∈ No )

Proof

Step	Hyp	Ref	Expression
1		0sno	⊢ 0s ∈ No
2	1 1	pm3.2i	⊢ ( 0s ∈ No ∧ 0s ∈ No )
3		mulsprop	⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( 0s ∈ No ∧ 0s ∈ No ) ∧ ( 0s ∈ No ∧ 0s ∈ No ) ) → ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 0s <s 0s ∧ 0s <s 0s ) → ( ( 0s ·s 0s ) -s ( 0s ·s 0s ) ) <s ( ( 0s ·s 0s ) -s ( 0s ·s 0s ) ) ) ) )
4	2 2 3	mp3an23	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐴 ·s 𝐵 ) ∈ No ∧ ( ( 0s <s 0s ∧ 0s <s 0s ) → ( ( 0s ·s 0s ) -s ( 0s ·s 0s ) ) <s ( ( 0s ·s 0s ) -s ( 0s ·s 0s ) ) ) ) )
5	4	simpld	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ·s 𝐵 ) ∈ No )