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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	ltdiv23neg.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	ltdiv23neg.3	⊢ ( 𝜑 → 𝐵 < 0 )
	ltdiv23neg.4	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	ltdiv23neg.5	⊢ ( 𝜑 → 𝐶 < 0 )
Assertion	ltdiv23neg	⊢ ( 𝜑 → ( ( 𝐴 / 𝐵 ) < 𝐶 ↔ ( 𝐴 / 𝐶 ) < 𝐵 ) )

Proof

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