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

Metamath Proof Explorer

Theorem lemul12a

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

Ref Expression
Assertion lemul12a ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷 ) → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷 ) ) → ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) )
2 simpll ⊢ ( ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ 𝐷 ∈ ℝ ) → 𝐶 ∈ ℝ )
3 2 ad2antlr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷 ) ) → 𝐶 ∈ ℝ )
4 simplrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷 ) ) → 𝐷 ∈ ℝ )
5 0re ⊢ 0 ∈ ℝ
6 letr ⊢ ( ( 0 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( 0 ≤ 𝐶 ∧ 𝐶 ≤ 𝐷 ) → 0 ≤ 𝐷 ) )
7 5 6 mp3an1 ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( 0 ≤ 𝐶 ∧ 𝐶 ≤ 𝐷 ) → 0 ≤ 𝐷 ) )
8 7 exp4b ⊢ ( 𝐶 ∈ ℝ → ( 𝐷 ∈ ℝ → ( 0 ≤ 𝐶 → ( 𝐶 ≤ 𝐷 → 0 ≤ 𝐷 ) ) ) )
9 8 com23 ⊢ ( 𝐶 ∈ ℝ → ( 0 ≤ 𝐶 → ( 𝐷 ∈ ℝ → ( 𝐶 ≤ 𝐷 → 0 ≤ 𝐷 ) ) ) )
10 9 imp41 ⊢ ( ( ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ 𝐷 ∈ ℝ ) ∧ 𝐶 ≤ 𝐷 ) → 0 ≤ 𝐷 )
11 10 ad2ant2l ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷 ) ) → 0 ≤ 𝐷 )
12 4 11 jca ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷 ) ) → ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) )
13 1 3 12 jca32 ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷 ) ) → ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) ) ) )
14 simpr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷 ) ) → ( 𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷 ) )
15 lemul12b ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) ) ) → ( ( 𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷 ) → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐷 ) ) )
16 13 14 15 sylc ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ 𝐷 ∈ ℝ ) ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷 ) ) → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐷 ) )
17 16 ex ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷 ) → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐷 ) ) )