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

Metamath Proof Explorer

Theorem ltmul12ad

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

Ref Expression
Hypotheses ltp1d.1 ⊢ φ → A ∈ ℝ
divgt0d.2 ⊢ φ → B ∈ ℝ
lemul1ad.3 ⊢ φ → C ∈ ℝ
ltmul12ad.3 ⊢ φ → D ∈ ℝ
ltmul12ad.4 ⊢ φ → 0 ≤ A
ltmul12ad.5 ⊢ φ → A < B
ltmul12ad.6 ⊢ φ → 0 ≤ C
ltmul12ad.7 ⊢ φ → C < D
Assertion ltmul12ad ⊢ φ → 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 ltmul12ad.4 ⊢ φ → 0 ≤ A
6 ltmul12ad.5 ⊢ φ → A < B
7 ltmul12ad.6 ⊢ φ → 0 ≤ C
8 ltmul12ad.7 ⊢ φ → C < D
9 1 2 jca ⊢ φ → A ∈ ℝ ∧ B ∈ ℝ
10 5 6 jca ⊢ φ → 0 ≤ A ∧ A < B
11 3 4 jca ⊢ φ → C ∈ ℝ ∧ D ∈ ℝ
12 7 8 jca ⊢ φ → 0 ≤ C ∧ C < D
13 ltmul12a ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ∧ A < B ∧ C ∈ ℝ ∧ D ∈ ℝ ∧ 0 ≤ C ∧ C < D → A ⁢ C < B ⁢ D
14 9 10 11 12 13 syl22anc ⊢ φ → A ⁢ C < B ⁢ D