Metamath Proof Explorer


Theorem sltsubsub3bd

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 sltsubsub3bd φ A - s C < s B - 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 1 2 3 4 sltsubsubbd φ A - s C < s B - s D A - s B < s C - s D
6 1 2 3 4 sltsubsub2bd φ A - s B < s C - s D D - s C < s B - s A
7 5 6 bitrd φ A - s C < s B - s D D - s C < s B - s A