Metamath Proof Explorer


Theorem sltsub1

Description: Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 4-Feb-2025)

Ref Expression
Assertion sltsub1 A No B No C No A < s B A - s C < s B - s C

Proof

Step Hyp Ref Expression
1 negscl C No + s C No
2 sltadd1 A No B No + s C No A < s B A + s + s C < s B + s + s C
3 1 2 syl3an3 A No B No C No A < s B A + s + s C < s B + s + s C
4 subsval A No C No A - s C = A + s + s C
5 4 3adant2 A No B No C No A - s C = A + s + s C
6 subsval B No C No B - s C = B + s + s C
7 6 3adant1 A No B No C No B - s C = B + s + s C
8 5 7 breq12d A No B No C No A - s C < s B - s C A + s + s C < s B + s + s C
9 3 8 bitr4d A No B No C No A < s B A - s C < s B - s C