Theorem slesubaddd

Description: Surreal less-than or equal relationship between subtraction and addition. (Contributed by Scott Fenton, 26-May-2025)

	Ref	Expression
Hypotheses	sltsubadd.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	sltsubadd.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	sltsubadd.3	⊢ ( 𝜑 → 𝐶 ∈ No )
Assertion	slesubaddd	⊢ ( 𝜑 → ( ( 𝐴 -s 𝐵 ) ≤s 𝐶 ↔ 𝐴 ≤s ( 𝐶 +s 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sltsubadd.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		sltsubadd.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		sltsubadd.3	⊢ ( 𝜑 → 𝐶 ∈ No )
4	3 2 1	sltaddsubd	⊢ ( 𝜑 → ( ( 𝐶 +s 𝐵 ) <s 𝐴 ↔ 𝐶 <s ( 𝐴 -s 𝐵 ) ) )
5	4	notbid	⊢ ( 𝜑 → ( ¬ ( 𝐶 +s 𝐵 ) <s 𝐴 ↔ ¬ 𝐶 <s ( 𝐴 -s 𝐵 ) ) )
6	3 2	addscld	⊢ ( 𝜑 → ( 𝐶 +s 𝐵 ) ∈ No )
7		slenlt	⊢ ( ( 𝐴 ∈ No ∧ ( 𝐶 +s 𝐵 ) ∈ No ) → ( 𝐴 ≤s ( 𝐶 +s 𝐵 ) ↔ ¬ ( 𝐶 +s 𝐵 ) <s 𝐴 ) )
8	1 6 7	syl2anc	⊢ ( 𝜑 → ( 𝐴 ≤s ( 𝐶 +s 𝐵 ) ↔ ¬ ( 𝐶 +s 𝐵 ) <s 𝐴 ) )
9	1 2	subscld	⊢ ( 𝜑 → ( 𝐴 -s 𝐵 ) ∈ No )
10		slenlt	⊢ ( ( ( 𝐴 -s 𝐵 ) ∈ No ∧ 𝐶 ∈ No ) → ( ( 𝐴 -s 𝐵 ) ≤s 𝐶 ↔ ¬ 𝐶 <s ( 𝐴 -s 𝐵 ) ) )
11	9 3 10	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 -s 𝐵 ) ≤s 𝐶 ↔ ¬ 𝐶 <s ( 𝐴 -s 𝐵 ) ) )
12	5 8 11	3bitr4rd	⊢ ( 𝜑 → ( ( 𝐴 -s 𝐵 ) ≤s 𝐶 ↔ 𝐴 ≤s ( 𝐶 +s 𝐵 ) ) )