Theorem ledivdivd

Description: Invert ratios of positive numbers and swap their ordering. (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 {ℝ}^{+}$$
	ledivdivd.4	$$⊢\phi \to D\in {ℝ}^{+}$$
	ledivdivd.5	$$⊢\phi \to \frac{A}{B}\le \frac{C}{D}$$
Assertion	ledivdivd	$$⊢\phi \to \frac{D}{C}\le \frac{B}{A}$$

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		ledivdivd.4	$$⊢\phi \to D\in {ℝ}^{+}$$
5		ledivdivd.5	$$⊢\phi \to \frac{A}{B}\le \frac{C}{D}$$
6	1	rpregt0d	$$⊢\phi \to \left(A\in ℝ\wedge 0<A\right)$$
7	2	rpregt0d	$$⊢\phi \to \left(B\in ℝ\wedge 0<B\right)$$
8	3	rpregt0d	$$⊢\phi \to \left(C\in ℝ\wedge 0<C\right)$$
9	4	rpregt0d	$$⊢\phi \to \left(D\in ℝ\wedge 0<D\right)$$
10		ledivdiv	$$⊢\left(\left(\left(A\in ℝ\wedge 0<A\right)\wedge \left(B\in ℝ\wedge 0<B\right)\right)\wedge \left(\left(C\in ℝ\wedge 0<C\right)\wedge \left(D\in ℝ\wedge 0<D\right)\right)\right)\to \left(\frac{A}{B}\le \frac{C}{D}\leftrightarrow \frac{D}{C}\le \frac{B}{A}\right)$$
11	6 7 8 9 10	syl22anc	$$⊢\phi \to \left(\frac{A}{B}\le \frac{C}{D}\leftrightarrow \frac{D}{C}\le \frac{B}{A}\right)$$
12	5 11	mpbid	$$⊢\phi \to \frac{D}{C}\le \frac{B}{A}$$