Metamath Proof Explorer


Theorem sltneg

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

Ref Expression
Assertion sltneg A No B No A < s B + s B < s + s A

Proof

Step Hyp Ref Expression
1 sltnegim A No B No A < s B + s B < s + s A
2 negscl B No + s B No
3 negscl A No + s A No
4 sltnegim + s B No + s A No + s B < s + s A + s + s A < s + s + s B
5 2 3 4 syl2anr A No B No + s B < s + s A + s + s A < s + s + s B
6 negnegs A No + s + s A = A
7 negnegs B No + s + s B = B
8 6 7 breqan12d A No B No + s + s A < s + s + s B A < s B
9 5 8 sylibd A No B No + s B < s + s A A < s B
10 1 9 impbid A No B No A < s B + s B < s + s A