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	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{\cdot }_{s}B\in \mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		0no	$$⊢0_s\in \mathrm{No}$$
2	1 1	pm3.2i	$$⊢\left(0_s\in \mathrm{No}\wedge 0_s\in \mathrm{No}\right)$$
3		mulsprop	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge \left(0_s\in \mathrm{No}\wedge 0_s\in \mathrm{No}\right)\wedge \left(0_s\in \mathrm{No}\wedge 0_s\in \mathrm{No}\right)\right)\to \left(A{\cdot }_{s}B\in \mathrm{No}\wedge \left(\left(0_s{<}_s{0}_s\wedge 0_s{<}_s{0}_s\right)\to \left(\left(0_s{\cdot }_s{0}_s\right){-}_s\left(0_s{\cdot }_s{0}_s\right)\right){<}_s\left(\left(0_s{\cdot }_s{0}_s\right){-}_s\left(0_s{\cdot }_s{0}_s\right)\right)\right)\right)$$
4	2 2 3	mp3an23	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(A{\cdot }_{s}B\in \mathrm{No}\wedge \left(\left(0_s{<}_s{0}_s\wedge 0_s{<}_s{0}_s\right)\to \left(\left(0_s{\cdot }_s{0}_s\right){-}_s\left(0_s{\cdot }_s{0}_s\right)\right){<}_s\left(\left(0_s{\cdot }_s{0}_s\right){-}_s\left(0_s{\cdot }_s{0}_s\right)\right)\right)\right)$$
5	4	simpld	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A{\cdot }_{s}B\in \mathrm{No}$$