Metamath Proof Explorer

Theorem lemul12b

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

Ref Expression
Assertion lemul12b ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧D∈ℝ∧0≤D→A≤B∧C≤D→A⁢C≤B⁢D

Proof

Step Hyp Ref Expression
1 lemul2a ⊢C∈ℝ∧D∈ℝ∧A∈ℝ∧0≤A∧C≤D→A⁢C≤A⁢D
2 1 ex ⊢C∈ℝ∧D∈ℝ∧A∈ℝ∧0≤A→C≤D→A⁢C≤A⁢D
3 2 3comr ⊢A∈ℝ∧0≤A∧C∈ℝ∧D∈ℝ→C≤D→A⁢C≤A⁢D
4 3 3expb ⊢A∈ℝ∧0≤A∧C∈ℝ∧D∈ℝ→C≤D→A⁢C≤A⁢D
5 4 adantrrr ⊢A∈ℝ∧0≤A∧C∈ℝ∧D∈ℝ∧0≤D→C≤D→A⁢C≤A⁢D
6 5 adantlr ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧D∈ℝ∧0≤D→C≤D→A⁢C≤A⁢D
7 lemul1a ⊢A∈ℝ∧B∈ℝ∧D∈ℝ∧0≤D∧A≤B→A⁢D≤B⁢D
8 7 ex ⊢A∈ℝ∧B∈ℝ∧D∈ℝ∧0≤D→A≤B→A⁢D≤B⁢D
9 8 ad4ant134 ⊢A∈ℝ∧0≤A∧B∈ℝ∧D∈ℝ∧0≤D→A≤B→A⁢D≤B⁢D
10 9 adantrl ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧D∈ℝ∧0≤D→A≤B→A⁢D≤B⁢D
11 6 10 anim12d ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧D∈ℝ∧0≤D→C≤D∧A≤B→A⁢C≤A⁢D∧A⁢D≤B⁢D
12 11 ancomsd ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧D∈ℝ∧0≤D→A≤B∧C≤D→A⁢C≤A⁢D∧A⁢D≤B⁢D
13 remulcl ⊢A∈ℝ∧C∈ℝ→A⁢C∈ℝ
14 13 adantlr ⊢A∈ℝ∧0≤A∧C∈ℝ→A⁢C∈ℝ
15 14 ad2ant2r ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧D∈ℝ∧0≤D→A⁢C∈ℝ
16 remulcl ⊢A∈ℝ∧D∈ℝ→A⁢D∈ℝ
17 16 ad2ant2r ⊢A∈ℝ∧0≤A∧D∈ℝ∧0≤D→A⁢D∈ℝ
18 17 ad2ant2rl ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧D∈ℝ∧0≤D→A⁢D∈ℝ
19 remulcl ⊢B∈ℝ∧D∈ℝ→B⁢D∈ℝ
20 19 adantrr ⊢B∈ℝ∧D∈ℝ∧0≤D→B⁢D∈ℝ
21 20 ad2ant2l ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧D∈ℝ∧0≤D→B⁢D∈ℝ
22 letr ⊢A⁢C∈ℝ∧A⁢D∈ℝ∧B⁢D∈ℝ→A⁢C≤A⁢D∧A⁢D≤B⁢D→A⁢C≤B⁢D
23 15 18 21 22 syl3anc ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧D∈ℝ∧0≤D→A⁢C≤A⁢D∧A⁢D≤B⁢D→A⁢C≤B⁢D
24 12 23 syld ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧D∈ℝ∧0≤D→A≤B∧C≤D→A⁢C≤B⁢D