This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ ( 𝐵 · 𝐶 ) < ( 𝐴 · 𝐶 ) ) )