Metamath Proof Explorer

Theorem sltsub2

Description: Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 4-Feb-2025)

Ref Expression
Assertion sltsub2 
|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( A  ( C -s B )

Proof

Step Hyp Ref Expression
1 negscl 
 |-  ( B e. No -> ( -us ` B ) e. No )
2 1 3ad2ant2 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( -us ` B ) e. No )
3 negscl 
 |-  ( A e. No -> ( -us ` A ) e. No )
4 3 3ad2ant1 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( -us ` A ) e. No )
5 simp3 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> C e. No )
6 2 4 5 sltadd2d 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( -us ` B )  ( C +s ( -us ` B ) )
7 sltneg 
 |-  ( ( A e. No /\ B e. No ) -> ( A  ( -us ` B )
8 7 3adant3 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A  ( -us ` B )
9 simp2 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> B e. No )
10 5 9 subsvald 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( C -s B ) = ( C +s ( -us ` B ) ) )
11 simp1 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> A e. No )
12 5 11 subsvald 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( C -s A ) = ( C +s ( -us ` A ) ) )
13 10 12 breq12d 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( C -s B )  ( C +s ( -us ` B ) )
14 6 8 13 3bitr4d 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A  ( C -s B )