Metamath Proof Explorer


Theorem sleadd1im

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

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

Proof

Step Hyp Ref Expression
1 sltadd1im ( ( 𝐵 No 𝐴 No 𝐶 No ) → ( 𝐵 <s 𝐴 → ( 𝐵 +s 𝐶 ) <s ( 𝐴 +s 𝐶 ) ) )
2 1 3com12 ( ( 𝐴 No 𝐵 No 𝐶 No ) → ( 𝐵 <s 𝐴 → ( 𝐵 +s 𝐶 ) <s ( 𝐴 +s 𝐶 ) ) )
3 sltnle ( ( 𝐵 No 𝐴 No ) → ( 𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵 ) )
4 3 ancoms ( ( 𝐴 No 𝐵 No ) → ( 𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵 ) )
5 4 3adant3 ( ( 𝐴 No 𝐵 No 𝐶 No ) → ( 𝐵 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝐵 ) )
6 addscl ( ( 𝐵 No 𝐶 No ) → ( 𝐵 +s 𝐶 ) ∈ No )
7 6 3adant1 ( ( 𝐴 No 𝐵 No 𝐶 No ) → ( 𝐵 +s 𝐶 ) ∈ No )
8 addscl ( ( 𝐴 No 𝐶 No ) → ( 𝐴 +s 𝐶 ) ∈ No )
9 sltnle ( ( ( 𝐵 +s 𝐶 ) ∈ No ∧ ( 𝐴 +s 𝐶 ) ∈ No ) → ( ( 𝐵 +s 𝐶 ) <s ( 𝐴 +s 𝐶 ) ↔ ¬ ( 𝐴 +s 𝐶 ) ≤s ( 𝐵 +s 𝐶 ) ) )
10 7 8 9 3imp3i2an ( ( 𝐴 No 𝐵 No 𝐶 No ) → ( ( 𝐵 +s 𝐶 ) <s ( 𝐴 +s 𝐶 ) ↔ ¬ ( 𝐴 +s 𝐶 ) ≤s ( 𝐵 +s 𝐶 ) ) )
11 2 5 10 3imtr3d ( ( 𝐴 No 𝐵 No 𝐶 No ) → ( ¬ 𝐴 ≤s 𝐵 → ¬ ( 𝐴 +s 𝐶 ) ≤s ( 𝐵 +s 𝐶 ) ) )
12 11 con4d ( ( 𝐴 No 𝐵 No 𝐶 No ) → ( ( 𝐴 +s 𝐶 ) ≤s ( 𝐵 +s 𝐶 ) → 𝐴 ≤s 𝐵 ) )