Theorem negscl

Description: The surreals are closed under negation. Theorem 6(ii) of Conway p. 18. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	negscl	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)\in \mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		0no	$$⊢0_s\in \mathrm{No}$$
2		negsprop	$$⊢\left(A\in \mathrm{No}\wedge 0_s\in \mathrm{No}\right)\to \left({+}_s\left(A\right)\in \mathrm{No}\wedge \left(A{<}_s{0}_s\to {+}_s\left(0_s\right){<}_s{+}_s\left(A\right)\right)\right)$$
3	1 2	mpan2	$$⊢A\in \mathrm{No}\to \left({+}_s\left(A\right)\in \mathrm{No}\wedge \left(A{<}_s{0}_s\to {+}_s\left(0_s\right){<}_s{+}_s\left(A\right)\right)\right)$$
4	3	simpld	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)\in \mathrm{No}$$