Theorem sleadd1im

Description: Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Assertion	sleadd1im	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A +s C ) <_s ( B +s C ) -> A <_s B ) )

Proof

Step	Hyp	Ref	Expression
1		sltadd1im	|- ( ( B e. No /\ A e. No /\ C e. No ) -> ( B ( B +s C )
2	1	3com12	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( B ( B +s C )
3		sltnle	|- ( ( B e. No /\ A e. No ) -> ( B -. A <_s B ) )
4	3	ancoms	|- ( ( A e. No /\ B e. No ) -> ( B -. A <_s B ) )
5	4	3adant3	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( B -. A <_s B ) )
6		addscl	|- ( ( B e. No /\ C e. No ) -> ( B +s C ) e. No )
7	6	3adant1	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( B +s C ) e. No )
8		addscl	|- ( ( A e. No /\ C e. No ) -> ( A +s C ) e. No )
9		sltnle	|- ( ( ( B +s C ) e. No /\ ( A +s C ) e. No ) -> ( ( B +s C ) -. ( A +s C ) <_s ( B +s C ) ) )
10	7 8 9	3imp3i2an	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( B +s C ) -. ( A +s C ) <_s ( B +s C ) ) )
11	2 5 10	3imtr3d	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( -. A <_s B -> -. ( A +s C ) <_s ( B +s C ) ) )
12	11	con4d	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A +s C ) <_s ( B +s C ) -> A <_s B ) )