Metamath Proof Explorer

Theorem sleadd2

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

Ref Expression
Assertion sleadd2 ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A ≤ s B ↔ C + s A ≤ s C + s B

Proof

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