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	$$⊢\phi \to A\in ℝ$$
	ltdiv23neg.2	$$⊢\phi \to B\in ℝ$$
	ltdiv23neg.3	$$⊢\phi \to B<0$$
	ltdiv23neg.4	$$⊢\phi \to C\in ℝ$$
	ltdiv23neg.5	$$⊢\phi \to C<0$$
Assertion	ltdiv23neg	$$⊢\phi \to \left(\frac{A}{B}<C\leftrightarrow \frac{A}{C}<B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ltdiv23neg.1	$$⊢\phi \to A\in ℝ$$
2		ltdiv23neg.2	$$⊢\phi \to B\in ℝ$$
3		ltdiv23neg.3	$$⊢\phi \to B<0$$
4		ltdiv23neg.4	$$⊢\phi \to C\in ℝ$$
5		ltdiv23neg.5	$$⊢\phi \to C<0$$
6	2 3	ltned	$$⊢\phi \to B\ne 0$$
7	1 2 6	redivcld	$$⊢\phi \to \frac{A}{B}\in ℝ$$
8	7 4 2 3	ltmulneg	$$⊢\phi \to \left(\frac{A}{B}<C\leftrightarrow CB<\left(\frac{A}{B}\right)B\right)$$
9		recn	$$⊢A\in ℝ\to A\in ℂ$$
10	1 9	syl	$$⊢\phi \to A\in ℂ$$
11		recn	$$⊢B\in ℝ\to B\in ℂ$$
12	2 11	syl	$$⊢\phi \to B\in ℂ$$
13	10 12 6	divcan1d	$$⊢\phi \to \left(\frac{A}{B}\right)B=A$$
14	13	breq2d	$$⊢\phi \to \left(CB<\left(\frac{A}{B}\right)B\leftrightarrow CB<A\right)$$
15		remulcl	$$⊢\left(C\in ℝ\wedge B\in ℝ\right)\to CB\in ℝ$$
16	4 2 15	syl2anc	$$⊢\phi \to CB\in ℝ$$
17	4 5	ltned	$$⊢\phi \to C\ne 0$$
18	4 17	rereccld	$$⊢\phi \to \frac{1}{C}\in ℝ$$
19	4 5	reclt0d	$$⊢\phi \to \frac{1}{C}<0$$
20	16 1 18 19	ltmulneg	$$⊢\phi \to \left(CB<A\leftrightarrow A\left(\frac{1}{C}\right)<CB\left(\frac{1}{C}\right)\right)$$
21		recn	$$⊢C\in ℝ\to C\in ℂ$$
22	4 21	syl	$$⊢\phi \to C\in ℂ$$
23	10 22 17	divrecd	$$⊢\phi \to \frac{A}{C}=A\left(\frac{1}{C}\right)$$
24	23	eqcomd	$$⊢\phi \to A\left(\frac{1}{C}\right)=\frac{A}{C}$$
25	22 12	mulcld	$$⊢\phi \to CB\in ℂ$$
26	25 22 17	divrecd	$$⊢\phi \to \frac{CB}{C}=CB\left(\frac{1}{C}\right)$$
27		divcan3	$$⊢\left(B\in ℂ\wedge C\in ℂ\wedge C\ne 0\right)\to \frac{CB}{C}=B$$
28	27	3expb	$$⊢\left(B\in ℂ\wedge \left(C\in ℂ\wedge C\ne 0\right)\right)\to \frac{CB}{C}=B$$
29	12 22 17 28	syl12anc	$$⊢\phi \to \frac{CB}{C}=B$$
30	26 29	eqtr3d	$$⊢\phi \to CB\left(\frac{1}{C}\right)=B$$
31	24 30	breq12d	$$⊢\phi \to \left(A\left(\frac{1}{C}\right)<CB\left(\frac{1}{C}\right)\leftrightarrow \frac{A}{C}<B\right)$$
32	20 31	bitrd	$$⊢\phi \to \left(CB<A\leftrightarrow \frac{A}{C}<B\right)$$
33	8 14 32	3bitrd	$$⊢\phi \to \left(\frac{A}{B}<C\leftrightarrow \frac{A}{C}<B\right)$$