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 ⊢ φ → A ∈ ℝ
ltmulneg.b ⊢ φ → B ∈ ℝ
ltmulneg.c ⊢ φ → C ∈ ℝ
ltmulneg.n ⊢ φ → C < 0
Assertion ltmulneg ⊢ φ → A < B ↔ B ⁢ C < A ⁢ C

Proof

Step Hyp Ref Expression
1 ltmulneg.a ⊢ φ → A ∈ ℝ
2 ltmulneg.b ⊢ φ → B ∈ ℝ
3 ltmulneg.c ⊢ φ → C ∈ ℝ
4 ltmulneg.n ⊢ φ → C < 0
5 3 4 negelrpd ⊢ φ → − C ∈ ℝ +
6 1 2 5 ltmul1d ⊢ φ → A < B ↔ A ⁢ − C < B ⁢ − C
7 3 renegcld ⊢ φ → − C ∈ ℝ
8 1 7 remulcld ⊢ φ → A ⁢ − C ∈ ℝ
9 2 7 remulcld ⊢ φ → B ⁢ − C ∈ ℝ
10 8 9 ltnegd ⊢ φ → A ⁢ − C < B ⁢ − C ↔ − B ⁢ − C < − A ⁢ − C
11 2 recnd ⊢ φ → B ∈ ℂ
12 7 recnd ⊢ φ → − C ∈ ℂ
13 11 12 mulneg2d ⊢ φ → B ⁢ − − C = − B ⁢ − C
14 3 recnd ⊢ φ → C ∈ ℂ
15 14 negnegd ⊢ φ → − − C = C
16 15 oveq2d ⊢ φ → B ⁢ − − C = B ⁢ C
17 13 16 eqtr3d ⊢ φ → − B ⁢ − C = B ⁢ C
18 1 recnd ⊢ φ → A ∈ ℂ
19 18 12 mulneg2d ⊢ φ → A ⁢ − − C = − A ⁢ − C
20 15 oveq2d ⊢ φ → A ⁢ − − C = A ⁢ C
21 19 20 eqtr3d ⊢ φ → − A ⁢ − C = A ⁢ C
22 17 21 breq12d ⊢ φ → − B ⁢ − C < − A ⁢ − C ↔ B ⁢ C < A ⁢ C
23 6 10 22 3bitrd ⊢ φ → A < B ↔ B ⁢ C < A ⁢ C