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	$$⊢\phi \to A\in \mathrm{No}$$
	sltsubadd.2	$$⊢\phi \to B\in \mathrm{No}$$
	sltsubadd.3	$$⊢\phi \to C\in \mathrm{No}$$
Assertion	slesubaddd	Could not format assertion : No typesetting found for |- ( ph -> ( ( A -s B ) <_s C <-> A <_s ( C +s B ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		sltsubadd.1	$$⊢\phi \to A\in \mathrm{No}$$
2		sltsubadd.2	$$⊢\phi \to B\in \mathrm{No}$$
3		sltsubadd.3	$$⊢\phi \to C\in \mathrm{No}$$
4	3 2 1	sltaddsubd	Could not format ( ph -> ( ( C +s B ) C ( ( C +s B ) C
5	4	notbid	Could not format ( ph -> ( -. ( C +s B ) -. C ( -. ( C +s B ) -. C
6	3 2	addscld	Could not format ( ph -> ( C +s B ) e. No ) : No typesetting found for |- ( ph -> ( C +s B ) e. No ) with typecode |-
7		slenlt	Could not format ( ( A e. No /\ ( C +s B ) e. No ) -> ( A <_s ( C +s B ) <-> -. ( C +s B ) ( A <_s ( C +s B ) <-> -. ( C +s B )
8	1 6 7	syl2anc	Could not format ( ph -> ( A <_s ( C +s B ) <-> -. ( C +s B ) ( A <_s ( C +s B ) <-> -. ( C +s B )
9	1 2	subscld	Could not format ( ph -> ( A -s B ) e. No ) : No typesetting found for |- ( ph -> ( A -s B ) e. No ) with typecode |-
10		slenlt	Could not format ( ( ( A -s B ) e. No /\ C e. No ) -> ( ( A -s B ) <_s C <-> -. C ( ( A -s B ) <_s C <-> -. C
11	9 3 10	syl2anc	Could not format ( ph -> ( ( A -s B ) <_s C <-> -. C ( ( A -s B ) <_s C <-> -. C
12	5 8 11	3bitr4rd	Could not format ( ph -> ( ( A -s B ) <_s C <-> A <_s ( C +s B ) ) ) : No typesetting found for |- ( ph -> ( ( A -s B ) <_s C <-> A <_s ( C +s B ) ) ) with typecode |-