Metamath Proof Explorer

Theorem lemul12a

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

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

Proof

Step Hyp Ref Expression
1 simpll ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ D ∈ ℝ ∧ A ≤ B ∧ C ≤ D → A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ
2 simpll ⊢ C ∈ ℝ ∧ 0 ≤ C ∧ D ∈ ℝ → C ∈ ℝ
3 2 ad2antlr ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ D ∈ ℝ ∧ A ≤ B ∧ C ≤ D → C ∈ ℝ
4 simplrr ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ D ∈ ℝ ∧ A ≤ B ∧ C ≤ D → D ∈ ℝ
5 0re ⊢ 0 ∈ ℝ
6 letr ⊢ 0 ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ → 0 ≤ C ∧ C ≤ D → 0 ≤ D
7 5 6 mp3an1 ⊢ C ∈ ℝ ∧ D ∈ ℝ → 0 ≤ C ∧ C ≤ D → 0 ≤ D
8 7 exp4b ⊢ C ∈ ℝ → D ∈ ℝ → 0 ≤ C → C ≤ D → 0 ≤ D
9 8 com23 ⊢ C ∈ ℝ → 0 ≤ C → D ∈ ℝ → C ≤ D → 0 ≤ D
10 9 imp41 ⊢ C ∈ ℝ ∧ 0 ≤ C ∧ D ∈ ℝ ∧ C ≤ D → 0 ≤ D
11 10 ad2ant2l ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ D ∈ ℝ ∧ A ≤ B ∧ C ≤ D → 0 ≤ D
12 4 11 jca ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ D ∈ ℝ ∧ A ≤ B ∧ C ≤ D → D ∈ ℝ ∧ 0 ≤ D
13 1 3 12 jca32 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ D ∈ ℝ ∧ A ≤ B ∧ C ≤ D → A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ ∧ 0 ≤ D
14 simpr ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ D ∈ ℝ ∧ A ≤ B ∧ C ≤ D → A ≤ B ∧ C ≤ D
15 lemul12b ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ ∧ 0 ≤ D → A ≤ B ∧ C ≤ D → A ⁢ C ≤ B ⁢ D
16 13 14 15 sylc ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ D ∈ ℝ ∧ A ≤ B ∧ C ≤ D → A ⁢ C ≤ B ⁢ D
17 16 ex ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 ≤ C ∧ D ∈ ℝ → A ≤ B ∧ C ≤ D → A ⁢ C ≤ B ⁢ D