Theorem lemuldiv4d

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

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

Proof

Step	Hyp	Ref	Expression
1		lemuldiv4d.1	$$⊢\phi \to B\le \frac{C}{A}$$
2		lemuldiv4d.2	$$⊢\phi \to 0<A$$
3		lemuldiv4d.3	$$⊢\phi \to A\in ℝ$$
4		lemuldiv4d.4	$$⊢\phi \to B\in ℝ$$
5		lemuldiv4d.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	7	bicomd	$$⊢\phi \to \left(B\le \frac{C}{A}\leftrightarrow BA\le C\right)$$
9	1 8	mpbid	$$⊢\phi \to BA\le C$$