Metamath Proof Explorer


Theorem negsex

Description: Every surreal has a negative. Note that this theorem, addscl , addscom , addsass , addsrid , and sltadd1im are the ordered Abelian group axioms. However, the surreals cannot be said to be an ordered Abelian group because No is a proper class. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion negsex A No x No A + s x = 0 s

Proof

Step Hyp Ref Expression
1 negscl A No + s A No
2 negsid A No A + s + s A = 0 s
3 oveq2 x = + s A A + s x = A + s + s A
4 3 eqeq1d x = + s A A + s x = 0 s A + s + s A = 0 s
5 4 rspcev + s A No A + s + s A = 0 s x No A + s x = 0 s
6 1 2 5 syl2anc A No x No A + s x = 0 s