Metamath Proof Explorer


Theorem sltaddsubd

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 sltaddsubd φ A + s B < s C A < s C - s B

Proof

Step Hyp Ref Expression
1 sltsubadd.1 φ A No
2 sltsubadd.2 φ B No
3 sltsubadd.3 φ C No
4 1 2 addscld φ A + s B No
5 4 3 2 sltsub1d φ A + s B < s C A + s B - s B < s C - s B
6 pncans A No B No A + s B - s B = A
7 1 2 6 syl2anc φ A + s B - s B = A
8 7 breq1d φ A + s B - s B < s C - s B A < s C - s B
9 5 8 bitrd φ A + s B < s C A < s C - s B