Theorem ltmulneg

Description: Multiplying by a negative number, swaps the order. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	ltmulneg.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	ltmulneg.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	ltmulneg.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	ltmulneg.n	⊢ ( 𝜑 → 𝐶 < 0 )
Assertion	ltmulneg	⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ ( 𝐵 · 𝐶 ) < ( 𝐴 · 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ltmulneg.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		ltmulneg.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		ltmulneg.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		ltmulneg.n	⊢ ( 𝜑 → 𝐶 < 0 )
5	3 4	negelrpd	⊢ ( 𝜑 → - 𝐶 ∈ ℝ+ )
6	1 2 5	ltmul1d	⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ ( 𝐴 · - 𝐶 ) < ( 𝐵 · - 𝐶 ) ) )
7	3	renegcld	⊢ ( 𝜑 → - 𝐶 ∈ ℝ )
8	1 7	remulcld	⊢ ( 𝜑 → ( 𝐴 · - 𝐶 ) ∈ ℝ )
9	2 7	remulcld	⊢ ( 𝜑 → ( 𝐵 · - 𝐶 ) ∈ ℝ )
10	8 9	ltnegd	⊢ ( 𝜑 → ( ( 𝐴 · - 𝐶 ) < ( 𝐵 · - 𝐶 ) ↔ - ( 𝐵 · - 𝐶 ) < - ( 𝐴 · - 𝐶 ) ) )
11	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
12	7	recnd	⊢ ( 𝜑 → - 𝐶 ∈ ℂ )
13	11 12	mulneg2d	⊢ ( 𝜑 → ( 𝐵 · - - 𝐶 ) = - ( 𝐵 · - 𝐶 ) )
14	3	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
15	14	negnegd	⊢ ( 𝜑 → - - 𝐶 = 𝐶 )
16	15	oveq2d	⊢ ( 𝜑 → ( 𝐵 · - - 𝐶 ) = ( 𝐵 · 𝐶 ) )
17	13 16	eqtr3d	⊢ ( 𝜑 → - ( 𝐵 · - 𝐶 ) = ( 𝐵 · 𝐶 ) )
18	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
19	18 12	mulneg2d	⊢ ( 𝜑 → ( 𝐴 · - - 𝐶 ) = - ( 𝐴 · - 𝐶 ) )
20	15	oveq2d	⊢ ( 𝜑 → ( 𝐴 · - - 𝐶 ) = ( 𝐴 · 𝐶 ) )
21	19 20	eqtr3d	⊢ ( 𝜑 → - ( 𝐴 · - 𝐶 ) = ( 𝐴 · 𝐶 ) )
22	17 21	breq12d	⊢ ( 𝜑 → ( - ( 𝐵 · - 𝐶 ) < - ( 𝐴 · - 𝐶 ) ↔ ( 𝐵 · 𝐶 ) < ( 𝐴 · 𝐶 ) ) )
23	6 10 22	3bitrd	⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ ( 𝐵 · 𝐶 ) < ( 𝐴 · 𝐶 ) ) )