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