Metamath Proof Explorer


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 No + s A No

Proof

Step Hyp Ref Expression
1 0sno 0 s No
2 negsprop A No 0 s No + s A No A < s 0 s + s 0 s < s + s A
3 1 2 mpan2 A No + s A No A < s 0 s + s 0 s < s + s A
4 3 simpld A No + s A No