Metamath Proof Explorer


Theorem subscl

Description: Closure law for surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion subscl A No B No A - s B No

Proof

Step Hyp Ref Expression
1 subsval A No B No A - s B = A + s + s B
2 negscl B No + s B No
3 addscl A No + s B No A + s + s B No
4 2 3 sylan2 A No B No A + s + s B No
5 1 4 eqeltrd A No B No A - s B No