Metamath Proof Explorer


Theorem sltsubadd2d

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

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

Proof

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