Theorem ltadds1im

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

	Ref	Expression
Assertion	ltadds1im	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( 𝐴 <s 𝐵 → ( 𝐴 +s 𝐶 ) <s ( 𝐵 +s 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		addsprop	⊢ ( ( 𝐶 ∈ No ∧ 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐶 +s 𝐴 ) ∈ No ∧ ( 𝐴 <s 𝐵 → ( 𝐴 +s 𝐶 ) <s ( 𝐵 +s 𝐶 ) ) ) )
2	1	3coml	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ( 𝐶 +s 𝐴 ) ∈ No ∧ ( 𝐴 <s 𝐵 → ( 𝐴 +s 𝐶 ) <s ( 𝐵 +s 𝐶 ) ) ) )
3	2	simprd	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( 𝐴 <s 𝐵 → ( 𝐴 +s 𝐶 ) <s ( 𝐵 +s 𝐶 ) ) )