Theorem ltdiv2d

Description: Division of a positive number by both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	rpred.1	$$⊢\phi \to A\in {ℝ}^{+}$$
	rpaddcld.1	$$⊢\phi \to B\in {ℝ}^{+}$$
	ltdiv2d.3	$$⊢\phi \to C\in {ℝ}^{+}$$
Assertion	ltdiv2d	$$⊢\phi \to \left(A<B\leftrightarrow \frac{C}{B}<\frac{C}{A}\right)$$

Proof

Step	Hyp	Ref	Expression
1		rpred.1	$$⊢\phi \to A\in {ℝ}^{+}$$
2		rpaddcld.1	$$⊢\phi \to B\in {ℝ}^{+}$$
3		ltdiv2d.3	$$⊢\phi \to C\in {ℝ}^{+}$$
4	1	rpregt0d	$$⊢\phi \to \left(A\in ℝ\wedge 0<A\right)$$
5	2	rpregt0d	$$⊢\phi \to \left(B\in ℝ\wedge 0<B\right)$$
6	3	rpregt0d	$$⊢\phi \to \left(C\in ℝ\wedge 0<C\right)$$
7		ltdiv2	$$⊢\left(\left(A\in ℝ\wedge 0<A\right)\wedge \left(B\in ℝ\wedge 0<B\right)\wedge \left(C\in ℝ\wedge 0<C\right)\right)\to \left(A<B\leftrightarrow \frac{C}{B}<\frac{C}{A}\right)$$
8	4 5 6 7	syl3anc	$$⊢\phi \to \left(A<B\leftrightarrow \frac{C}{B}<\frac{C}{A}\right)$$