Theorem lemuldiv3d

Description: 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypotheses	lemuldiv3d.1	$$⊢\phi \to BA\le C$$
	lemuldiv3d.2	$$⊢\phi \to 0<A$$
	lemuldiv3d.3	$$⊢\phi \to A\in ℝ$$
	lemuldiv3d.4	$$⊢\phi \to B\in ℝ$$
	lemuldiv3d.5	$$⊢\phi \to C\in ℝ$$
Assertion	lemuldiv3d	$$⊢\phi \to B\le \frac{C}{A}$$

Proof

Step	Hyp	Ref	Expression
1		lemuldiv3d.1	$$⊢\phi \to BA\le C$$
2		lemuldiv3d.2	$$⊢\phi \to 0<A$$
3		lemuldiv3d.3	$$⊢\phi \to A\in ℝ$$
4		lemuldiv3d.4	$$⊢\phi \to B\in ℝ$$
5		lemuldiv3d.5	$$⊢\phi \to C\in ℝ$$
6		lemuldiv	$$⊢\left(B\in ℝ\wedge C\in ℝ\wedge \left(A\in ℝ\wedge 0<A\right)\right)\to \left(BA\le C\leftrightarrow B\le \frac{C}{A}\right)$$
7	4 5 3 2 6	syl112anc	$$⊢\phi \to \left(BA\le C\leftrightarrow B\le \frac{C}{A}\right)$$
8	1 7	mpbid	$$⊢\phi \to B\le \frac{C}{A}$$