Theorem ltmulnegs1d

Description: Multiplication of both sides of surreal less-than by a negative number. (Contributed by Scott Fenton, 14-Mar-2025)

	Ref	Expression
Hypotheses	ltmulnegs.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	ltmulnegs.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	ltmulnegs.3	⊢ ( 𝜑 → 𝐶 ∈ No )
	ltmulnegs.4	⊢ ( 𝜑 → 𝐶 <s 0s )
Assertion	ltmulnegs1d	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 ↔ ( 𝐵 ·s 𝐶 ) <s ( 𝐴 ·s 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ltmulnegs.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		ltmulnegs.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		ltmulnegs.3	⊢ ( 𝜑 → 𝐶 ∈ No )
4		ltmulnegs.4	⊢ ( 𝜑 → 𝐶 <s 0s )
5	1 3	mulnegs2d	⊢ ( 𝜑 → ( 𝐴 ·s ( -us ‘ 𝐶 ) ) = ( -us ‘ ( 𝐴 ·s 𝐶 ) ) )
6	2 3	mulnegs2d	⊢ ( 𝜑 → ( 𝐵 ·s ( -us ‘ 𝐶 ) ) = ( -us ‘ ( 𝐵 ·s 𝐶 ) ) )
7	5 6	breq12d	⊢ ( 𝜑 → ( ( 𝐴 ·s ( -us ‘ 𝐶 ) ) <s ( 𝐵 ·s ( -us ‘ 𝐶 ) ) ↔ ( -us ‘ ( 𝐴 ·s 𝐶 ) ) <s ( -us ‘ ( 𝐵 ·s 𝐶 ) ) ) )
8	3	negscld	⊢ ( 𝜑 → ( -us ‘ 𝐶 ) ∈ No )
9		neg0s	⊢ ( -us ‘ 0s ) = 0s
10		0no	⊢ 0s ∈ No
11	10	a1i	⊢ ( 𝜑 → 0s ∈ No )
12	3 11	ltnegsd	⊢ ( 𝜑 → ( 𝐶 <s 0s ↔ ( -us ‘ 0s ) <s ( -us ‘ 𝐶 ) ) )
13	4 12	mpbid	⊢ ( 𝜑 → ( -us ‘ 0s ) <s ( -us ‘ 𝐶 ) )
14	9 13	eqbrtrrid	⊢ ( 𝜑 → 0s <s ( -us ‘ 𝐶 ) )
15	1 2 8 14	ltmuls1d	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 ↔ ( 𝐴 ·s ( -us ‘ 𝐶 ) ) <s ( 𝐵 ·s ( -us ‘ 𝐶 ) ) ) )
16	2 3	mulscld	⊢ ( 𝜑 → ( 𝐵 ·s 𝐶 ) ∈ No )
17	1 3	mulscld	⊢ ( 𝜑 → ( 𝐴 ·s 𝐶 ) ∈ No )
18	16 17	ltnegsd	⊢ ( 𝜑 → ( ( 𝐵 ·s 𝐶 ) <s ( 𝐴 ·s 𝐶 ) ↔ ( -us ‘ ( 𝐴 ·s 𝐶 ) ) <s ( -us ‘ ( 𝐵 ·s 𝐶 ) ) ) )
19	7 15 18	3bitr4d	⊢ ( 𝜑 → ( 𝐴 <s 𝐵 ↔ ( 𝐵 ·s 𝐶 ) <s ( 𝐴 ·s 𝐶 ) ) )