Theorem lemul12bd

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

	Ref	Expression
Hypotheses	ltp1d.1	$$⊢\phi \to A\in ℝ$$
	divgt0d.2	$$⊢\phi \to B\in ℝ$$
	lemul1ad.3	$$⊢\phi \to C\in ℝ$$
	ltmul12ad.3	$$⊢\phi \to D\in ℝ$$
	lemul12bd.4	$$⊢\phi \to 0\le A$$
	lemul12bd.5	$$⊢\phi \to 0\le D$$
	lemul12bd.6	$$⊢\phi \to A\le B$$
	lemul12bd.7	$$⊢\phi \to C\le D$$
Assertion	lemul12bd	$$⊢\phi \to AC\le BD$$

Proof

Step	Hyp	Ref	Expression
1		ltp1d.1	$$⊢\phi \to A\in ℝ$$
2		divgt0d.2	$$⊢\phi \to B\in ℝ$$
3		lemul1ad.3	$$⊢\phi \to C\in ℝ$$
4		ltmul12ad.3	$$⊢\phi \to D\in ℝ$$
5		lemul12bd.4	$$⊢\phi \to 0\le A$$
6		lemul12bd.5	$$⊢\phi \to 0\le D$$
7		lemul12bd.6	$$⊢\phi \to A\le B$$
8		lemul12bd.7	$$⊢\phi \to C\le D$$
9	1 5	jca	$$⊢\phi \to \left(A\in ℝ\wedge 0\le A\right)$$
10	4 6	jca	$$⊢\phi \to \left(D\in ℝ\wedge 0\le D\right)$$
11		lemul12b	$$⊢\left(\left(\left(A\in ℝ\wedge 0\le A\right)\wedge B\in ℝ\right)\wedge \left(C\in ℝ\wedge \left(D\in ℝ\wedge 0\le D\right)\right)\right)\to \left(\left(A\le B\wedge C\le D\right)\to AC\le BD\right)$$
12	9 2 3 10 11	syl22anc	$$⊢\phi \to \left(\left(A\le B\wedge C\le D\right)\to AC\le BD\right)$$
13	7 8 12	mp2and	$$⊢\phi \to AC\le BD$$