Theorem sltaddsubd

Description: Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 28-Feb-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	sltaddsubd	Could not format assertion : No typesetting found for |- ( ph -> ( ( A +s B ) A

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	1 2	addscld	Could not format ( ph -> ( A +s B ) e. No ) : No typesetting found for |- ( ph -> ( A +s B ) e. No ) with typecode |-
5	4 3 2	sltsub1d	Could not format ( ph -> ( ( A +s B ) ( ( A +s B ) -s B ) ( ( A +s B ) ( ( A +s B ) -s B )
6		pncans	Could not format ( ( A e. No /\ B e. No ) -> ( ( A +s B ) -s B ) = A ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( ( A +s B ) -s B ) = A ) with typecode |-
7	1 2 6	syl2anc	Could not format ( ph -> ( ( A +s B ) -s B ) = A ) : No typesetting found for |- ( ph -> ( ( A +s B ) -s B ) = A ) with typecode |-
8	7	breq1d	Could not format ( ph -> ( ( ( A +s B ) -s B ) A ( ( ( A +s B ) -s B ) A
9	5 8	bitrd	Could not format ( ph -> ( ( A +s B ) A ( ( A +s B ) A