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 φANo
sltsubadd.2 φBNo
sltsubadd.3 φCNo
Assertion sltsubaddd φA-sB<sCA<sC+sB

Proof

Step Hyp Ref Expression
1 sltsubadd.1 φANo
2 sltsubadd.2 φBNo
3 sltsubadd.3 φCNo
4 1 2 subscld φA-sBNo
5 4 3 2 sltadd1d φA-sB<sCA-sB+sB<sC+sB
6 npcans ANoBNoA-sB+sB=A
7 1 2 6 syl2anc φA-sB+sB=A
8 7 breq1d φA-sB+sB<sC+sBA<sC+sB
9 5 8 bitrd φA-sB<sCA<sC+sB