Metamath Proof Explorer


Theorem sltsubsubbd

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

Ref Expression
Hypotheses sltsubsubbd.1 φ A No
sltsubsubbd.2 φ B No
sltsubsubbd.3 φ C No
sltsubsubbd.4 φ D No
Assertion sltsubsubbd φ 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 npcans A No C No A - s C + s C = A
6 1 3 5 syl2anc φ A - s C + s C = A
7 npcans A No B No A - s B + s B = A
8 1 2 7 syl2anc φ A - s B + s B = A
9 6 8 eqtr4d φ A - s C + s C = A - s B + s B
10 2 3 addscomd φ B + s C = C + s B
11 10 oveq1d φ B + s C + s + s D = C + s B + s + s D
12 2 4 subsvald φ B - s D = B + s + s D
13 12 oveq1d φ B - s D + s C = B + s + s D + s C
14 4 negscld φ + s D No
15 2 14 3 adds32d φ B + s + s D + s C = B + s C + s + s D
16 13 15 eqtrd φ B - s D + s C = B + s C + s + s D
17 3 4 subsvald φ C - s D = C + s + s D
18 17 oveq1d φ C - s D + s B = C + s + s D + s B
19 3 14 2 adds32d φ C + s + s D + s B = C + s B + s + s D
20 18 19 eqtrd φ C - s D + s B = C + s B + s + s D
21 11 16 20 3eqtr4d φ B - s D + s C = C - s D + s B
22 9 21 breq12d φ A - s C + s C < s B - s D + s C A - s B + s B < s C - s D + s B
23 1 3 subscld φ A - s C No
24 2 4 subscld φ B - s D No
25 23 24 3 sltadd1d φ A - s C < s B - s D A - s C + s C < s B - s D + s C
26 1 2 subscld φ A - s B No
27 3 4 subscld φ C - s D No
28 26 27 2 sltadd1d φ A - s B < s C - s D A - s B + s B < s C - s D + s B
29 22 25 28 3bitr4d φ A - s C < s B - s D A - s B < s C - s D