Metamath Proof Explorer


Theorem negsval2

Description: Surreal negation in terms of subtraction. (Contributed by Scott Fenton, 15-Apr-2025)

Ref Expression
Assertion negsval2 A No + s A = 0 s - s A

Proof

Step Hyp Ref Expression
1 0sno 0 s No
2 subsval 0 s No A No 0 s - s A = 0 s + s + s A
3 1 2 mpan A No 0 s - s A = 0 s + s + s A
4 negscl A No + s A No
5 addslid + s A No 0 s + s + s A = + s A
6 4 5 syl A No 0 s + s + s A = + s A
7 3 6 eqtr2d A No + s A = 0 s - s A