Theorem lediv12ad

Description: Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	ltmul1d.1	$$⊢\phi \to A\in ℝ$$
	ltmul1d.2	$$⊢\phi \to B\in ℝ$$
	ltmul1d.3	$$⊢\phi \to C\in {ℝ}^{+}$$
	lediv12ad.4	$$⊢\phi \to D\in ℝ$$
	lediv12ad.5	$$⊢\phi \to 0\le A$$
	lediv12ad.6	$$⊢\phi \to A\le B$$
	lediv12ad.7	$$⊢\phi \to C\le D$$
Assertion	lediv12ad	$$⊢\phi \to \frac{A}{D}\le \frac{B}{C}$$

Proof

Step	Hyp	Ref	Expression
1		ltmul1d.1	$$⊢\phi \to A\in ℝ$$
2		ltmul1d.2	$$⊢\phi \to B\in ℝ$$
3		ltmul1d.3	$$⊢\phi \to C\in {ℝ}^{+}$$
4		lediv12ad.4	$$⊢\phi \to D\in ℝ$$
5		lediv12ad.5	$$⊢\phi \to 0\le A$$
6		lediv12ad.6	$$⊢\phi \to A\le B$$
7		lediv12ad.7	$$⊢\phi \to C\le D$$
8	1 2	jca	$$⊢\phi \to \left(A\in ℝ\wedge B\in ℝ\right)$$
9	5 6	jca	$$⊢\phi \to \left(0\le A\wedge A\le B\right)$$
10	3	rpred	$$⊢\phi \to C\in ℝ$$
11	10 4	jca	$$⊢\phi \to \left(C\in ℝ\wedge D\in ℝ\right)$$
12	3	rpgt0d	$$⊢\phi \to 0<C$$
13	12 7	jca	$$⊢\phi \to \left(0<C\wedge C\le D\right)$$
14		lediv12a	$$⊢\left(\left(\left(A\in ℝ\wedge B\in ℝ\right)\wedge \left(0\le A\wedge A\le B\right)\right)\wedge \left(\left(C\in ℝ\wedge D\in ℝ\right)\wedge \left(0<C\wedge C\le D\right)\right)\right)\to \frac{A}{D}\le \frac{B}{C}$$
15	8 9 11 13 14	syl22anc	$$⊢\phi \to \frac{A}{D}\le \frac{B}{C}$$