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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
divgt0d.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
lemul1ad.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
ltmul12ad.3 ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
lemul12bd.4 ⊢ ( 𝜑 → 0 ≤ 𝐴 )
lemul12bd.5 ⊢ ( 𝜑 → 0 ≤ 𝐷 )
lemul12bd.6 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
lemul12bd.7 ⊢ ( 𝜑 → 𝐶 ≤ 𝐷 )
Assertion lemul12bd ( 𝜑 → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐷 ) )

Proof

Step Hyp Ref Expression
1 ltp1d.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 divgt0d.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 lemul1ad.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4 ltmul12ad.3 ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
5 lemul12bd.4 ⊢ ( 𝜑 → 0 ≤ 𝐴 )
6 lemul12bd.5 ⊢ ( 𝜑 → 0 ≤ 𝐷 )
7 lemul12bd.6 ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
8 lemul12bd.7 ⊢ ( 𝜑 → 𝐶 ≤ 𝐷 )
9 1 5 jca ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
10 4 6 jca ⊢ ( 𝜑 → ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) )
11 lemul12b ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) ) ) → ( ( 𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷 ) → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐷 ) ) )
12 9 2 3 10 11 syl22anc ⊢ ( 𝜑 → ( ( 𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷 ) → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐷 ) ) )
13 7 8 12 mp2and ⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐷 ) )