Metamath Proof Explorer


Theorem slesubsubbd

Description: Equivalence for the surreal less-than or equal relationship between differences. (Contributed by Scott Fenton, 7-Mar-2025)

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

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 2 1 4 3 sltsubsub3bd φ B - s D < s A - s C C - s D < s A - s B
6 5 notbid φ ¬ B - s D < s A - s C ¬ C - s D < s A - s B
7 1 3 subscld φ A - s C No
8 2 4 subscld φ B - s D No
9 slenlt A - s C No B - s D No A - s C s B - s D ¬ B - s D < s A - s C
10 7 8 9 syl2anc φ A - s C s B - s D ¬ B - s D < s A - s C
11 1 2 subscld φ A - s B No
12 3 4 subscld φ C - s D No
13 slenlt A - s B No C - s D No A - s B s C - s D ¬ C - s D < s A - s B
14 11 12 13 syl2anc φ A - s B s C - s D ¬ C - s D < s A - s B
15 6 10 14 3bitr4d φ A - s C s B - s D A - s B s C - s D