Metamath Proof Explorer


Theorem sleneg

Description: Negative of both sides of surreal less-than or equal. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion sleneg A No B No A s B + s B s + s A

Proof

Step Hyp Ref Expression
1 sltneg B No A No B < s A + s A < s + s B
2 1 ancoms A No B No B < s A + s A < s + s B
3 2 notbid A No B No ¬ B < s A ¬ + s A < s + s B
4 slenlt A No B No A s B ¬ B < s A
5 negscl B No + s B No
6 negscl A No + s A No
7 slenlt + s B No + s A No + s B s + s A ¬ + s A < s + s B
8 5 6 7 syl2anr A No B No + s B s + s A ¬ + s A < s + s B
9 3 4 8 3bitr4d A No B No A s B + s B s + s A