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