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

Proof

Step Hyp Ref Expression
1 addscom ⊢ A ∈ No ∧ C ∈ No → A + s C = C + s A
2 1 3adant2 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A + s C = C + s A
3 addscom ⊢ B ∈ No ∧ C ∈ No → B + s C = C + s B
4 3 3adant1 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → B + s C = C + s B
5 2 4 breq12d ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A + s C ≤ s B + s C ↔ C + s A ≤ s C + s B
6 sleadd1im ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A + s C ≤ s B + s C → A ≤ s B
7 5 6 sylbird ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → C + s A ≤ s C + s B → A ≤ s B