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 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A + s C ≤ s B + s C → A ≤ s B

Proof

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