Theorem ltdiv23ii

Description: Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999)

	Ref	Expression
Hypotheses	ltplus1.1	$$⊢A\in ℝ$$
	prodgt0.2	$$⊢B\in ℝ$$
	ltmul1.3	$$⊢C\in ℝ$$
	ltdiv23i.4	$$⊢0<B$$
	ltdiv23i.5	$$⊢0<C$$
Assertion	ltdiv23ii	$$⊢\frac{A}{B}<C\leftrightarrow \frac{A}{C}<B$$

Proof

Step	Hyp	Ref	Expression
1		ltplus1.1	$$⊢A\in ℝ$$
2		prodgt0.2	$$⊢B\in ℝ$$
3		ltmul1.3	$$⊢C\in ℝ$$
4		ltdiv23i.4	$$⊢0<B$$
5		ltdiv23i.5	$$⊢0<C$$
6	1 2 3	ltdiv23i	$$⊢\left(0<B\wedge 0<C\right)\to \left(\frac{A}{B}<C\leftrightarrow \frac{A}{C}<B\right)$$
7	4 5 6	mp2an	$$⊢\frac{A}{B}<C\leftrightarrow \frac{A}{C}<B$$