Metamath Proof Explorer

Theorem lemul12a

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

Ref Expression
Assertion lemul12a ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧0≤C∧D∈ℝ→A≤B∧C≤D→A⁢C≤B⁢D

Proof

Step Hyp Ref Expression
1 simpll ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧0≤C∧D∈ℝ∧A≤B∧C≤D→A∈ℝ∧0≤A∧B∈ℝ
2 simpll ⊢C∈ℝ∧0≤C∧D∈ℝ→C∈ℝ
3 2 ad2antlr ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧0≤C∧D∈ℝ∧A≤B∧C≤D→C∈ℝ
4 simplrr ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧0≤C∧D∈ℝ∧A≤B∧C≤D→D∈ℝ
5 0re ⊢0∈ℝ
6 letr ⊢0∈ℝ∧C∈ℝ∧D∈ℝ→0≤C∧C≤D→0≤D
7 5 6 mp3an1 ⊢C∈ℝ∧D∈ℝ→0≤C∧C≤D→0≤D
8 7 exp4b ⊢C∈ℝ→D∈ℝ→0≤C→C≤D→0≤D
9 8 com23 ⊢C∈ℝ→0≤C→D∈ℝ→C≤D→0≤D
10 9 imp41 ⊢C∈ℝ∧0≤C∧D∈ℝ∧C≤D→0≤D
11 10 ad2ant2l ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧0≤C∧D∈ℝ∧A≤B∧C≤D→0≤D
12 4 11 jca ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧0≤C∧D∈ℝ∧A≤B∧C≤D→D∈ℝ∧0≤D
13 1 3 12 jca32 ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧0≤C∧D∈ℝ∧A≤B∧C≤D→A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧D∈ℝ∧0≤D
14 simpr ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧0≤C∧D∈ℝ∧A≤B∧C≤D→A≤B∧C≤D
15 lemul12b ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧D∈ℝ∧0≤D→A≤B∧C≤D→A⁢C≤B⁢D
16 13 14 15 sylc ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧0≤C∧D∈ℝ∧A≤B∧C≤D→A⁢C≤B⁢D
17 16 ex ⊢A∈ℝ∧0≤A∧B∈ℝ∧C∈ℝ∧0≤C∧D∈ℝ→A≤B∧C≤D→A⁢C≤B⁢D