Metamath Proof Explorer


Theorem sleadd2im

Description: Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Assertion sleadd2im ( ( 𝐴 No 𝐵 No 𝐶 No ) → ( ( 𝐶 +s 𝐴 ) ≤s ( 𝐶 +s 𝐵 ) → 𝐴 ≤s 𝐵 ) )

Proof

Step Hyp Ref Expression
1 addscom ( ( 𝐴 No 𝐶 No ) → ( 𝐴 +s 𝐶 ) = ( 𝐶 +s 𝐴 ) )
2 1 3adant2 ( ( 𝐴 No 𝐵 No 𝐶 No ) → ( 𝐴 +s 𝐶 ) = ( 𝐶 +s 𝐴 ) )
3 addscom ( ( 𝐵 No 𝐶 No ) → ( 𝐵 +s 𝐶 ) = ( 𝐶 +s 𝐵 ) )
4 3 3adant1 ( ( 𝐴 No 𝐵 No 𝐶 No ) → ( 𝐵 +s 𝐶 ) = ( 𝐶 +s 𝐵 ) )
5 2 4 breq12d ( ( 𝐴 No 𝐵 No 𝐶 No ) → ( ( 𝐴 +s 𝐶 ) ≤s ( 𝐵 +s 𝐶 ) ↔ ( 𝐶 +s 𝐴 ) ≤s ( 𝐶 +s 𝐵 ) ) )
6 sleadd1im ( ( 𝐴 No 𝐵 No 𝐶 No ) → ( ( 𝐴 +s 𝐶 ) ≤s ( 𝐵 +s 𝐶 ) → 𝐴 ≤s 𝐵 ) )
7 5 6 sylbird ( ( 𝐴 No 𝐵 No 𝐶 No ) → ( ( 𝐶 +s 𝐴 ) ≤s ( 𝐶 +s 𝐵 ) → 𝐴 ≤s 𝐵 ) )