This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lemul12bd

Description: Comparison of product of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses ltp1d.1 ⊢ φ → A ∈ ℝ
divgt0d.2 ⊢ φ → B ∈ ℝ
lemul1ad.3 ⊢ φ → C ∈ ℝ
ltmul12ad.3 ⊢ φ → D ∈ ℝ
lemul12bd.4 ⊢ φ → 0 ≤ A
lemul12bd.5 ⊢ φ → 0 ≤ D
lemul12bd.6 ⊢ φ → A ≤ B
lemul12bd.7 ⊢ φ → C ≤ D
Assertion lemul12bd ⊢ φ → A ⁢ C ≤ B ⁢ D

Proof

Step Hyp Ref Expression
1 ltp1d.1 ⊢ φ → A ∈ ℝ
2 divgt0d.2 ⊢ φ → B ∈ ℝ
3 lemul1ad.3 ⊢ φ → C ∈ ℝ
4 ltmul12ad.3 ⊢ φ → D ∈ ℝ
5 lemul12bd.4 ⊢ φ → 0 ≤ A
6 lemul12bd.5 ⊢ φ → 0 ≤ D
7 lemul12bd.6 ⊢ φ → A ≤ B
8 lemul12bd.7 ⊢ φ → C ≤ D
9 1 5 jca ⊢ φ → A ∈ ℝ ∧ 0 ≤ A
10 4 6 jca ⊢ φ → D ∈ ℝ ∧ 0 ≤ D
11 lemul12b ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ D ∈ ℝ ∧ 0 ≤ D → A ≤ B ∧ C ≤ D → A ⁢ C ≤ B ⁢ D
12 9 2 3 10 11 syl22anc ⊢ φ → A ≤ B ∧ C ≤ D → A ⁢ C ≤ B ⁢ D
13 7 8 12 mp2and ⊢ φ → A ⁢ C ≤ B ⁢ D