Metamath Proof Explorer

Theorem ltdiv23neg

Description: Swap denominator with other side of 'less than', when both are negative. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses ltdiv23neg.1 ⊢ φ → A ∈ ℝ
ltdiv23neg.2 ⊢ φ → B ∈ ℝ
ltdiv23neg.3 ⊢ φ → B < 0
ltdiv23neg.4 ⊢ φ → C ∈ ℝ
ltdiv23neg.5 ⊢ φ → C < 0
Assertion ltdiv23neg ⊢ φ → A B < C ↔ A C < B

Proof

Step Hyp Ref Expression
1 ltdiv23neg.1 ⊢ φ → A ∈ ℝ
2 ltdiv23neg.2 ⊢ φ → B ∈ ℝ
3 ltdiv23neg.3 ⊢ φ → B < 0
4 ltdiv23neg.4 ⊢ φ → C ∈ ℝ
5 ltdiv23neg.5 ⊢ φ → C < 0
6 2 3 ltned ⊢ φ → B ≠ 0
7 1 2 6 redivcld ⊢ φ → A B ∈ ℝ
8 7 4 2 3 ltmulneg ⊢ φ → A B < C ↔ C ⁢ B < A B ⁢ B
9 recn ⊢ A ∈ ℝ → A ∈ ℂ
10 1 9 syl ⊢ φ → A ∈ ℂ
11 recn ⊢ B ∈ ℝ → B ∈ ℂ
12 2 11 syl ⊢ φ → B ∈ ℂ
13 10 12 6 divcan1d ⊢ φ → A B ⁢ B = A
14 13 breq2d ⊢ φ → C ⁢ B < A B ⁢ B ↔ C ⁢ B < A
15 remulcl ⊢ C ∈ ℝ ∧ B ∈ ℝ → C ⁢ B ∈ ℝ
16 4 2 15 syl2anc ⊢ φ → C ⁢ B ∈ ℝ
17 4 5 ltned ⊢ φ → C ≠ 0
18 4 17 rereccld ⊢ φ → 1 C ∈ ℝ
19 4 5 reclt0d ⊢ φ → 1 C < 0
20 16 1 18 19 ltmulneg ⊢ φ → C ⁢ B < A ↔ A ⁢ 1 C < C ⁢ B ⁢ 1 C
21 recn ⊢ C ∈ ℝ → C ∈ ℂ
22 4 21 syl ⊢ φ → C ∈ ℂ
23 10 22 17 divrecd ⊢ φ → A C = A ⁢ 1 C
24 23 eqcomd ⊢ φ → A ⁢ 1 C = A C
25 22 12 mulcld ⊢ φ → C ⁢ B ∈ ℂ
26 25 22 17 divrecd ⊢ φ → C ⁢ B C = C ⁢ B ⁢ 1 C
27 divcan3 ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ B C = B
28 27 3expb ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ B C = B
29 12 22 17 28 syl12anc ⊢ φ → C ⁢ B C = B
30 26 29 eqtr3d ⊢ φ → C ⁢ B ⁢ 1 C = B
31 24 30 breq12d ⊢ φ → A ⁢ 1 C < C ⁢ B ⁢ 1 C ↔ A C < B
32 20 31 bitrd ⊢ φ → C ⁢ B < A ↔ A C < B
33 8 14 32 3bitrd ⊢ φ → A B < C ↔ A C < B