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 ≤ 𝐶 ) ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 ≤ 𝐵 ∧ 𝐶 ≤ 𝐷 ) → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐷 ) ) )