Theorem sltsub2

Description: Subtraction from both sides of surreal less-than. (Contributed by Scott Fenton, 4-Feb-2025)

	Ref	Expression
Assertion	sltsub2	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( 𝐴 <s 𝐵 ↔ ( 𝐶 -s 𝐵 ) <s ( 𝐶 -s 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		negscl	⊢ ( 𝐵 ∈ No → ( -us ‘ 𝐵 ) ∈ No )
2	1	3ad2ant2	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( -us ‘ 𝐵 ) ∈ No )
3		negscl	⊢ ( 𝐴 ∈ No → ( -us ‘ 𝐴 ) ∈ No )
4	3	3ad2ant1	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( -us ‘ 𝐴 ) ∈ No )
5		simp3	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → 𝐶 ∈ No )
6	2 4 5	sltadd2d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ↔ ( 𝐶 +s ( -us ‘ 𝐵 ) ) <s ( 𝐶 +s ( -us ‘ 𝐴 ) ) ) )
7		sltneg	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 ↔ ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) )
8	7	3adant3	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( 𝐴 <s 𝐵 ↔ ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) )
9		simp2	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → 𝐵 ∈ No )
10	5 9	subsvald	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( 𝐶 -s 𝐵 ) = ( 𝐶 +s ( -us ‘ 𝐵 ) ) )
11		simp1	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → 𝐴 ∈ No )
12	5 11	subsvald	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( 𝐶 -s 𝐴 ) = ( 𝐶 +s ( -us ‘ 𝐴 ) ) )
13	10 12	breq12d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ( 𝐶 -s 𝐵 ) <s ( 𝐶 -s 𝐴 ) ↔ ( 𝐶 +s ( -us ‘ 𝐵 ) ) <s ( 𝐶 +s ( -us ‘ 𝐴 ) ) ) )
14	6 8 13	3bitr4d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( 𝐴 <s 𝐵 ↔ ( 𝐶 -s 𝐵 ) <s ( 𝐶 -s 𝐴 ) ) )