Theorem ltaddsubs2d

Description: Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 28-Feb-2025)

	Ref	Expression
Hypotheses	ltsubadds.1	$$⊢\phi \to A\in \mathrm{No}$$
	ltsubadds.2	$$⊢\phi \to B\in \mathrm{No}$$
	ltsubadds.3	$$⊢\phi \to C\in \mathrm{No}$$
Assertion	ltaddsubs2d	$$⊢\phi \to \left(\left(A{+}_{s}B\right){<}_{s}C\leftrightarrow B{<}_s\left(C{-}_{s}A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ltsubadds.1	$$⊢\phi \to A\in \mathrm{No}$$
2		ltsubadds.2	$$⊢\phi \to B\in \mathrm{No}$$
3		ltsubadds.3	$$⊢\phi \to C\in \mathrm{No}$$
4	1 2	addscomd	$$⊢\phi \to A{+}_{s}B=B{+}_{s}A$$
5	4	breq1d	$$⊢\phi \to \left(\left(A{+}_{s}B\right){<}_{s}C\leftrightarrow \left(B{+}_{s}A\right){<}_{s}C\right)$$
6	2 1 3	ltaddsubsd	$$⊢\phi \to \left(\left(B{+}_{s}A\right){<}_{s}C\leftrightarrow B{<}_s\left(C{-}_{s}A\right)\right)$$
7	5 6	bitrd	$$⊢\phi \to \left(\left(A{+}_{s}B\right){<}_{s}C\leftrightarrow B{<}_s\left(C{-}_{s}A\right)\right)$$