Metamath Proof Explorer


Theorem sltsubsub2bd

Description: Equivalence for the surreal less-than relationship between differences. (Contributed by Scott Fenton, 21-Feb-2025)

Ref Expression
Hypotheses sltsubsubbd.1 φ A No
sltsubsubbd.2 φ B No
sltsubsubbd.3 φ C No
sltsubsubbd.4 φ D No
Assertion sltsubsub2bd φ A - s B < s C - s D D - s C < s B - s A

Proof

Step Hyp Ref Expression
1 sltsubsubbd.1 φ A No
2 sltsubsubbd.2 φ B No
3 sltsubsubbd.3 φ C No
4 sltsubsubbd.4 φ D No
5 4 3 subscld φ D - s C No
6 2 1 subscld φ B - s A No
7 5 6 sltnegd φ D - s C < s B - s A + s B - s A < s + s D - s C
8 2 1 negsubsdi2d φ + s B - s A = A - s B
9 4 3 negsubsdi2d φ + s D - s C = C - s D
10 8 9 breq12d φ + s B - s A < s + s D - s C A - s B < s C - s D
11 7 10 bitr2d φ A - s B < s C - s D D - s C < s B - s A