Metamath Proof Explorer


Theorem sltaddsub2d

Description: Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 28-Feb-2025)

Ref Expression
Hypotheses sltsubadd.1 φ A No
sltsubadd.2 φ B No
sltsubadd.3 φ C No
Assertion sltaddsub2d φ A + s B < s C B < s C - s A

Proof

Step Hyp Ref Expression
1 sltsubadd.1 φ A No
2 sltsubadd.2 φ B No
3 sltsubadd.3 φ C No
4 1 2 addscomd φ A + s B = B + s A
5 4 breq1d φ A + s B < s C B + s A < s C
6 2 1 3 sltaddsubd φ B + s A < s C B < s C - s A
7 5 6 bitrd φ A + s B < s C B < s C - s A