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 
|- ( ph -> A e. No )
sltsubsubbd.2 
|- ( ph -> B e. No )
sltsubsubbd.3 
|- ( ph -> C e. No )
sltsubsubbd.4 
|- ( ph -> D e. No )
Assertion sltsubsubbd 
|- ( ph -> ( ( A -s C )  ( A -s B )

Proof

Step Hyp Ref Expression
1 sltsubsubbd.1 
 |-  ( ph -> A e. No )
2 sltsubsubbd.2 
 |-  ( ph -> B e. No )
3 sltsubsubbd.3 
 |-  ( ph -> C e. No )
4 sltsubsubbd.4 
 |-  ( ph -> D e. No )
5 npcans 
 |-  ( ( A e. No /\ C e. No ) -> ( ( A -s C ) +s C ) = A )
6 1 3 5 syl2anc 
 |-  ( ph -> ( ( A -s C ) +s C ) = A )
7 npcans 
 |-  ( ( A e. No /\ B e. No ) -> ( ( A -s B ) +s B ) = A )
8 1 2 7 syl2anc 
 |-  ( ph -> ( ( A -s B ) +s B ) = A )
9 6 8 eqtr4d 
 |-  ( ph -> ( ( A -s C ) +s C ) = ( ( A -s B ) +s B ) )
10 2 3 addscomd 
 |-  ( ph -> ( B +s C ) = ( C +s B ) )
11 10 oveq1d 
 |-  ( ph -> ( ( B +s C ) +s ( -us ` D ) ) = ( ( C +s B ) +s ( -us ` D ) ) )
12 2 4 subsvald 
 |-  ( ph -> ( B -s D ) = ( B +s ( -us ` D ) ) )
13 12 oveq1d 
 |-  ( ph -> ( ( B -s D ) +s C ) = ( ( B +s ( -us ` D ) ) +s C ) )
14 4 negscld 
 |-  ( ph -> ( -us ` D ) e. No )
15 2 14 3 adds32d 
 |-  ( ph -> ( ( B +s ( -us ` D ) ) +s C ) = ( ( B +s C ) +s ( -us ` D ) ) )
16 13 15 eqtrd 
 |-  ( ph -> ( ( B -s D ) +s C ) = ( ( B +s C ) +s ( -us ` D ) ) )
17 3 4 subsvald 
 |-  ( ph -> ( C -s D ) = ( C +s ( -us ` D ) ) )
18 17 oveq1d 
 |-  ( ph -> ( ( C -s D ) +s B ) = ( ( C +s ( -us ` D ) ) +s B ) )
19 3 14 2 adds32d 
 |-  ( ph -> ( ( C +s ( -us ` D ) ) +s B ) = ( ( C +s B ) +s ( -us ` D ) ) )
20 18 19 eqtrd 
 |-  ( ph -> ( ( C -s D ) +s B ) = ( ( C +s B ) +s ( -us ` D ) ) )
21 11 16 20 3eqtr4d 
 |-  ( ph -> ( ( B -s D ) +s C ) = ( ( C -s D ) +s B ) )
22 9 21 breq12d 
 |-  ( ph -> ( ( ( A -s C ) +s C )  ( ( A -s B ) +s B )
23 1 3 subscld 
 |-  ( ph -> ( A -s C ) e. No )
24 2 4 subscld 
 |-  ( ph -> ( B -s D ) e. No )
25 23 24 3 sltadd1d 
 |-  ( ph -> ( ( A -s C )  ( ( A -s C ) +s C )
26 1 2 subscld 
 |-  ( ph -> ( A -s B ) e. No )
27 3 4 subscld 
 |-  ( ph -> ( C -s D ) e. No )
28 26 27 2 sltadd1d 
 |-  ( ph -> ( ( A -s B )  ( ( A -s B ) +s B )
29 22 25 28 3bitr4d 
 |-  ( ph -> ( ( A -s C )  ( A -s B )