Metamath Proof Explorer


Theorem negsidd

Description: Surreal addition of a number and its negative. Theorem 4(iii) of Conway p. 17. (Contributed by Scott Fenton, 5-Feb-2025)

Ref Expression
Hypothesis negsidd.1 φ A No
Assertion negsidd φ A + s + s A = 0 s

Proof

Step Hyp Ref Expression
1 negsidd.1 φ A No
2 negsid A No A + s + s A = 0 s
3 1 2 syl φ A + s + s A = 0 s