Theorem lediv2ad

Description: Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	rpred.1	$$⊢\phi \to A\in {ℝ}^{+}$$
	rpaddcld.1	$$⊢\phi \to B\in {ℝ}^{+}$$
	lediv2ad.3	$$⊢\phi \to C\in ℝ$$
	lediv2ad.4	$$⊢\phi \to 0\le C$$
	lediv2ad.5	$$⊢\phi \to A\le B$$
Assertion	lediv2ad	$$⊢\phi \to \frac{C}{B}\le \frac{C}{A}$$

Proof

Step	Hyp	Ref	Expression
1		rpred.1	$$⊢\phi \to A\in {ℝ}^{+}$$
2		rpaddcld.1	$$⊢\phi \to B\in {ℝ}^{+}$$
3		lediv2ad.3	$$⊢\phi \to C\in ℝ$$
4		lediv2ad.4	$$⊢\phi \to 0\le C$$
5		lediv2ad.5	$$⊢\phi \to A\le B$$
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 4	jca	$$⊢\phi \to \left(C\in ℝ\wedge 0\le C\right)$$
9		lediv2a	$$⊢\left(\left(\left(A\in ℝ\wedge 0<A\right)\wedge \left(B\in ℝ\wedge 0<B\right)\wedge \left(C\in ℝ\wedge 0\le C\right)\right)\wedge A\le B\right)\to \frac{C}{B}\le \frac{C}{A}$$
10	6 7 8 5 9	syl31anc	$$⊢\phi \to \frac{C}{B}\le \frac{C}{A}$$