Theorem ltaddsubs2d

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

	Ref	Expression
Hypotheses	ltsubadds.1	|- ( ph -> A e. No )
	ltsubadds.2	|- ( ph -> B e. No )
	ltsubadds.3	|- ( ph -> C e. No )
Assertion	ltaddsubs2d	|- ( ph -> ( ( A +s B ) B

Proof

Step	Hyp	Ref	Expression
1		ltsubadds.1	|- ( ph -> A e. No )
2		ltsubadds.2	|- ( ph -> B e. No )
3		ltsubadds.3	|- ( ph -> C e. No )
4	1 2	addscomd	|- ( ph -> ( A +s B ) = ( B +s A ) )
5	4	breq1d	|- ( ph -> ( ( A +s B ) ( B +s A )
6	2 1 3	ltaddsubsd	|- ( ph -> ( ( B +s A ) B
7	5 6	bitrd	|- ( ph -> ( ( A +s B ) B