Metamath Proof Explorer


Theorem subsid

Description: Subtraction of a surreal from itself. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion subsid A No A - s A = 0 s

Proof

Step Hyp Ref Expression
1 subsval A No A No A - s A = A + s + s A
2 1 anidms A No A - s A = A + s + s A
3 negsid A No A + s + s A = 0 s
4 2 3 eqtrd A No A - s A = 0 s