Metamath Proof Explorer

Theorem sltadd2

Description: Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 sleadd2 
 |-  ( ( B e. No /\ A e. No /\ C e. No ) -> ( B <_s A <-> ( C +s B ) <_s ( C +s A ) ) )
2 1 3com12 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( B <_s A <-> ( C +s B ) <_s ( C +s A ) ) )
3 2 notbid 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( -. B <_s A <-> -. ( C +s B ) <_s ( C +s A ) ) )
4 sltnle 
 |-  ( ( A e. No /\ B e. No ) -> ( A  -. B <_s A ) )
5 4 3adant3 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A  -. B <_s A ) )
6 simp3 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> C e. No )
7 simp1 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> A e. No )
8 6 7 addscld 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( C +s A ) e. No )
9 simp2 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> B e. No )
10 6 9 addscld 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( C +s B ) e. No )
11 sltnle 
 |-  ( ( ( C +s A ) e. No /\ ( C +s B ) e. No ) -> ( ( C +s A )  -. ( C +s B ) <_s ( C +s A ) ) )
12 8 10 11 syl2anc 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( C +s A )  -. ( C +s B ) <_s ( C +s A ) ) )
13 3 5 12 3bitr4d 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A  ( C +s A )