Theorem lemulge12d

Description: Multiplication by a number greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	ltp1d.1	$$⊢\phi \to A\in ℝ$$
	divgt0d.2	$$⊢\phi \to B\in ℝ$$
	lemulge11d.3	$$⊢\phi \to 0\le A$$
	lemulge11d.4	$$⊢\phi \to 1\le B$$
Assertion	lemulge12d	$$⊢\phi \to A\le BA$$

Proof

Step	Hyp	Ref	Expression
1		ltp1d.1	$$⊢\phi \to A\in ℝ$$
2		divgt0d.2	$$⊢\phi \to B\in ℝ$$
3		lemulge11d.3	$$⊢\phi \to 0\le A$$
4		lemulge11d.4	$$⊢\phi \to 1\le B$$
5		lemulge12	$$⊢\left(\left(A\in ℝ\wedge B\in ℝ\right)\wedge \left(0\le A\wedge 1\le B\right)\right)\to A\le BA$$
6	1 2 3 4 5	syl22anc	$$⊢\phi \to A\le BA$$