Theorem ltnegs

Description: Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	ltnegs	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 ↔ ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ltnegsim	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) )
2		negscl	⊢ ( 𝐵 ∈ No → ( -us ‘ 𝐵 ) ∈ No )
3		negscl	⊢ ( 𝐴 ∈ No → ( -us ‘ 𝐴 ) ∈ No )
4		ltnegsim	⊢ ( ( ( -us ‘ 𝐵 ) ∈ No ∧ ( -us ‘ 𝐴 ) ∈ No ) → ( ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) → ( -us ‘ ( -us ‘ 𝐴 ) ) <s ( -us ‘ ( -us ‘ 𝐵 ) ) ) )
5	2 3 4	syl2anr	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) → ( -us ‘ ( -us ‘ 𝐴 ) ) <s ( -us ‘ ( -us ‘ 𝐵 ) ) ) )
6		negnegs	⊢ ( 𝐴 ∈ No → ( -us ‘ ( -us ‘ 𝐴 ) ) = 𝐴 )
7		negnegs	⊢ ( 𝐵 ∈ No → ( -us ‘ ( -us ‘ 𝐵 ) ) = 𝐵 )
8	6 7	breqan12d	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( -us ‘ ( -us ‘ 𝐴 ) ) <s ( -us ‘ ( -us ‘ 𝐵 ) ) ↔ 𝐴 <s 𝐵 ) )
9	5 8	sylibd	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) → 𝐴 <s 𝐵 ) )
10	1 9	impbid	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 ↔ ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) )