Metamath Proof Explorer


Theorem sltsubaddd

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 sltsubaddd φ 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 subscld φ A - s B No
5 4 3 2 sltadd1d φ A - s B < s C A - s B + s B < s C + s B
6 npcans 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