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	|- ( ph -> A e. No )
	sltsubadd.2	|- ( ph -> B e. No )
	sltsubadd.3	|- ( ph -> C e. No )
Assertion	slesubaddd	|- ( ph -> ( ( A -s B ) <_s C <-> A <_s ( C +s B ) ) )

Proof

Step	Hyp	Ref	Expression
1		sltsubadd.1	|- ( ph -> A e. No )
2		sltsubadd.2	|- ( ph -> B e. No )
3		sltsubadd.3	|- ( ph -> C e. No )
4	3 2 1	sltaddsubd	|- ( ph -> ( ( C +s B ) C
5	4	notbid	|- ( ph -> ( -. ( C +s B ) -. C
6	3 2	addscld	|- ( ph -> ( C +s B ) e. No )
7		slenlt	|- ( ( A e. No /\ ( C +s B ) e. No ) -> ( A <_s ( C +s B ) <-> -. ( C +s B )
8	1 6 7	syl2anc	|- ( ph -> ( A <_s ( C +s B ) <-> -. ( C +s B )
9	1 2	subscld	|- ( ph -> ( A -s B ) e. No )
10		slenlt	|- ( ( ( A -s B ) e. No /\ C e. No ) -> ( ( A -s B ) <_s C <-> -. C
11	9 3 10	syl2anc	|- ( ph -> ( ( A -s B ) <_s C <-> -. C
12	5 8 11	3bitr4rd	|- ( ph -> ( ( A -s B ) <_s C <-> A <_s ( C +s B ) ) )