Metamath Proof Explorer


Theorem negnegs

Description: A surreal is equal to the negative of its negative. Theorem 4(ii) of Conway p. 17. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion negnegs A No + s + s A = A

Proof

Step Hyp Ref Expression
1 negscl A No + s A No
2 1 negsidd A No + s A + s + s + s A = 0 s
3 1 negscld A No + s + s A No
4 3 1 addscomd A No + s + s A + s + s A = + s A + s + s + s A
5 negsid A No A + s + s A = 0 s
6 2 4 5 3eqtr4d A No + s + s A + s + s A = A + s + s A
7 id A No A No
8 3 7 1 addscan2d A No + s + s A + s + s A = A + s + s A + s + s A = A
9 6 8 mpbid A No + s + s A = A