Metamath Proof Explorer

Theorem ltadds1im

Description: Surreal less-than is preserved under addition. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Assertion ltadds1im ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A < s B → A + s C < s B + s C

Proof

Step Hyp Ref Expression
1 addsprop ⊢ C ∈ No ∧ A ∈ No ∧ B ∈ No → C + s A ∈ No ∧ A < s B → A + s C < s B + s C
2 1 3coml ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → C + s A ∈ No ∧ A < s B → A + s C < s B + s C
3 2 simprd ⊢ A ∈ No ∧ B ∈ No ∧ C ∈ No → A < s B → A + s C < s B + s C