Theorem lemul12ad

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 ℝ$$
	lemul12ad.4	$$⊢\phi \to 0\le A$$
	lemul12ad.5	$$⊢\phi \to 0\le C$$
	lemul12ad.6	$$⊢\phi \to A\le B$$
	lemul12ad.7	$$⊢\phi \to C\le D$$
Assertion	lemul12ad	$$⊢\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		lemul12ad.4	$$⊢\phi \to 0\le A$$
6		lemul12ad.5	$$⊢\phi \to 0\le C$$
7		lemul12ad.6	$$⊢\phi \to A\le B$$
8		lemul12ad.7	$$⊢\phi \to C\le D$$
9	1 5	jca	$$⊢\phi \to \left(A\in ℝ\wedge 0\le A\right)$$
10	3 6	jca	$$⊢\phi \to \left(C\in ℝ\wedge 0\le C\right)$$
11		lemul12a	$$⊢\left(\left(\left(A\in ℝ\wedge 0\le A\right)\wedge B\in ℝ\right)\wedge \left(\left(C\in ℝ\wedge 0\le C\right)\wedge D\in ℝ\right)\right)\to \left(\left(A\le B\wedge C\le D\right)\to AC\le BD\right)$$
12	9 2 10 4 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$$