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

Metamath Proof Explorer

Theorem lediv12ad

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

Ref Expression
Hypotheses ltmul1d.1 ⊢ φ → A ∈ ℝ
ltmul1d.2 ⊢ φ → B ∈ ℝ
ltmul1d.3 ⊢ φ → C ∈ ℝ +
lediv12ad.4 ⊢ φ → D ∈ ℝ
lediv12ad.5 ⊢ φ → 0 ≤ A
lediv12ad.6 ⊢ φ → A ≤ B
lediv12ad.7 ⊢ φ → C ≤ D
Assertion lediv12ad ⊢ φ → A D ≤ B C

Proof

Step Hyp Ref Expression
1 ltmul1d.1 ⊢ φ → A ∈ ℝ
2 ltmul1d.2 ⊢ φ → B ∈ ℝ
3 ltmul1d.3 ⊢ φ → C ∈ ℝ +
4 lediv12ad.4 ⊢ φ → D ∈ ℝ
5 lediv12ad.5 ⊢ φ → 0 ≤ A
6 lediv12ad.6 ⊢ φ → A ≤ B
7 lediv12ad.7 ⊢ φ → C ≤ D
8 1 2 jca ⊢ φ → A ∈ ℝ ∧ B ∈ ℝ
9 5 6 jca ⊢ φ → 0 ≤ A ∧ A ≤ B
10 3 rpred ⊢ φ → C ∈ ℝ
11 10 4 jca ⊢ φ → C ∈ ℝ ∧ D ∈ ℝ
12 3 rpgt0d ⊢ φ → 0 < C
13 12 7 jca ⊢ φ → 0 < C ∧ C ≤ D
14 lediv12a ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A ∧ A ≤ B ∧ C ∈ ℝ ∧ D ∈ ℝ ∧ 0 < C ∧ C ≤ D → A D ≤ B C
15 8 9 11 13 14 syl22anc ⊢ φ → A D ≤ B C