Metamath Proof Explorer


Theorem sltnegd

Description: Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 14-Mar-2025)

Ref Expression
Hypotheses sltnegd.1 φ A No
sltnegd.2 φ B No
Assertion sltnegd φ A < s B + s B < s + s A

Proof

Step Hyp Ref Expression
1 sltnegd.1 φ A No
2 sltnegd.2 φ B No
3 sltneg A No B No A < s B + s B < s + s A
4 1 2 3 syl2anc φ A < s B + s B < s + s A