# Metamath Proof Explorer

## Theorem lemul12b

Description: Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008)

Ref Expression
Assertion 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 {A}{C}\le {B}{D}\right)$

### Proof

Step Hyp Ref Expression
1 lemul2a ${⊢}\left(\left({C}\in ℝ\wedge {D}\in ℝ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\wedge {C}\le {D}\right)\to {A}{C}\le {A}{D}$
2 1 ex ${⊢}\left({C}\in ℝ\wedge {D}\in ℝ\wedge \left({A}\in ℝ\wedge 0\le {A}\right)\right)\to \left({C}\le {D}\to {A}{C}\le {A}{D}\right)$
3 2 3comr ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {C}\in ℝ\wedge {D}\in ℝ\right)\to \left({C}\le {D}\to {A}{C}\le {A}{D}\right)$
4 3 3expb ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\to \left({C}\le {D}\to {A}{C}\le {A}{D}\right)$
5 4 adantrrr ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({C}\in ℝ\wedge \left({D}\in ℝ\wedge 0\le {D}\right)\right)\right)\to \left({C}\le {D}\to {A}{C}\le {A}{D}\right)$
6 5 adantlr ${⊢}\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({C}\le {D}\to {A}{C}\le {A}{D}\right)$
7 lemul1a ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({D}\in ℝ\wedge 0\le {D}\right)\right)\wedge {A}\le {B}\right)\to {A}{D}\le {B}{D}$
8 7 ex ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({D}\in ℝ\wedge 0\le {D}\right)\right)\to \left({A}\le {B}\to {A}{D}\le {B}{D}\right)$
9 8 ad4ant134 ${⊢}\left(\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {B}\in ℝ\right)\wedge \left({D}\in ℝ\wedge 0\le {D}\right)\right)\to \left({A}\le {B}\to {A}{D}\le {B}{D}\right)$
10 9 adantrl ${⊢}\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({A}\le {B}\to {A}{D}\le {B}{D}\right)$
11 6 10 anim12d ${⊢}\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({C}\le {D}\wedge {A}\le {B}\right)\to \left({A}{C}\le {A}{D}\wedge {A}{D}\le {B}{D}\right)\right)$
12 11 ancomsd ${⊢}\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 \left({A}{C}\le {A}{D}\wedge {A}{D}\le {B}{D}\right)\right)$
13 remulcl ${⊢}\left({A}\in ℝ\wedge {C}\in ℝ\right)\to {A}{C}\in ℝ$
14 13 adantlr ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge {C}\in ℝ\right)\to {A}{C}\in ℝ$
15 14 ad2ant2r ${⊢}\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 {A}{C}\in ℝ$
16 remulcl ${⊢}\left({A}\in ℝ\wedge {D}\in ℝ\right)\to {A}{D}\in ℝ$
17 16 ad2ant2r ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({D}\in ℝ\wedge 0\le {D}\right)\right)\to {A}{D}\in ℝ$
18 17 ad2ant2rl ${⊢}\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 {A}{D}\in ℝ$
19 remulcl ${⊢}\left({B}\in ℝ\wedge {D}\in ℝ\right)\to {B}{D}\in ℝ$
20 19 adantrr ${⊢}\left({B}\in ℝ\wedge \left({D}\in ℝ\wedge 0\le {D}\right)\right)\to {B}{D}\in ℝ$
21 20 ad2ant2l ${⊢}\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 {B}{D}\in ℝ$
22 letr ${⊢}\left({A}{C}\in ℝ\wedge {A}{D}\in ℝ\wedge {B}{D}\in ℝ\right)\to \left(\left({A}{C}\le {A}{D}\wedge {A}{D}\le {B}{D}\right)\to {A}{C}\le {B}{D}\right)$
23 15 18 21 22 syl3anc ${⊢}\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}{C}\le {A}{D}\wedge {A}{D}\le {B}{D}\right)\to {A}{C}\le {B}{D}\right)$
24 12 23 syld ${⊢}\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 {A}{C}\le {B}{D}\right)$