Metamath Proof Explorer

Theorem ltmul12a

Description: Comparison of product of two positive numbers. (Contributed by NM, 30-Dec-2005)

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

Proof

Step Hyp Ref Expression
1 simplll ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ∧ ( 0 ≤ 𝐶 ∧ 𝐶 < 𝐷 ) ) ) → 𝐴 ∈ ℝ )
2 simpllr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ∧ ( 0 ≤ 𝐶 ∧ 𝐶 < 𝐷 ) ) ) → 𝐵 ∈ ℝ )
3 simpll ⊢ ( ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ∧ ( 0 ≤ 𝐶 ∧ 𝐶 < 𝐷 ) ) → 𝐶 ∈ ℝ )
4 simprl ⊢ ( ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ∧ ( 0 ≤ 𝐶 ∧ 𝐶 < 𝐷 ) ) → 0 ≤ 𝐶 )
5 3 4 jca ⊢ ( ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ∧ ( 0 ≤ 𝐶 ∧ 𝐶 < 𝐷 ) ) → ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
6 5 ad2ant2l ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ∧ ( 0 ≤ 𝐶 ∧ 𝐶 < 𝐷 ) ) ) → ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
7 ltle ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 → 𝐴 ≤ 𝐵 ) )
8 7 imp ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) → 𝐴 ≤ 𝐵 )
9 8 adantrl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → 𝐴 ≤ 𝐵 )
10 9 ad2ant2r ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ∧ ( 0 ≤ 𝐶 ∧ 𝐶 < 𝐷 ) ) ) → 𝐴 ≤ 𝐵 )
11 lemul1a ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) )
12 1 2 6 10 11 syl31anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ∧ ( 0 ≤ 𝐶 ∧ 𝐶 < 𝐷 ) ) ) → ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) )
13 simplrl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → 𝐶 ∈ ℝ )
14 simplrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → 𝐷 ∈ ℝ )
15 simpllr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → 𝐵 ∈ ℝ )
16 0re ⊢ 0 ∈ ℝ
17 lelttr ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) → 0 < 𝐵 ) )
18 16 17 mp3an1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) → 0 < 𝐵 ) )
19 18 imp ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → 0 < 𝐵 )
20 19 adantlr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → 0 < 𝐵 )
21 ltmul2 ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐶 < 𝐷 ↔ ( 𝐵 · 𝐶 ) < ( 𝐵 · 𝐷 ) ) )
22 13 14 15 20 21 syl112anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) → ( 𝐶 < 𝐷 ↔ ( 𝐵 · 𝐶 ) < ( 𝐵 · 𝐷 ) ) )
23 22 biimpa ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ 𝐶 < 𝐷 ) → ( 𝐵 · 𝐶 ) < ( 𝐵 · 𝐷 ) )
24 23 anasss ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ∧ 𝐶 < 𝐷 ) ) → ( 𝐵 · 𝐶 ) < ( 𝐵 · 𝐷 ) )
25 24 adantrrl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ∧ ( 0 ≤ 𝐶 ∧ 𝐶 < 𝐷 ) ) ) → ( 𝐵 · 𝐶 ) < ( 𝐵 · 𝐷 ) )
26 remulcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 𝐶 ) ∈ ℝ )
27 26 ad2ant2r ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐴 · 𝐶 ) ∈ ℝ )
28 remulcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 · 𝐶 ) ∈ ℝ )
29 28 ad2ant2lr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐵 · 𝐶 ) ∈ ℝ )
30 remulcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 𝐵 · 𝐷 ) ∈ ℝ )
31 30 ad2ant2l ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐵 · 𝐷 ) ∈ ℝ )
32 lelttr ⊢ ( ( ( 𝐴 · 𝐶 ) ∈ ℝ ∧ ( 𝐵 · 𝐶 ) ∈ ℝ ∧ ( 𝐵 · 𝐷 ) ∈ ℝ ) → ( ( ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ∧ ( 𝐵 · 𝐶 ) < ( 𝐵 · 𝐷 ) ) → ( 𝐴 · 𝐶 ) < ( 𝐵 · 𝐷 ) ) )
33 27 29 31 32 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ∧ ( 𝐵 · 𝐶 ) < ( 𝐵 · 𝐷 ) ) → ( 𝐴 · 𝐶 ) < ( 𝐵 · 𝐷 ) ) )
34 33 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ∧ ( 0 ≤ 𝐶 ∧ 𝐶 < 𝐷 ) ) ) → ( ( ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ∧ ( 𝐵 · 𝐶 ) < ( 𝐵 · 𝐷 ) ) → ( 𝐴 · 𝐶 ) < ( 𝐵 · 𝐷 ) ) )
35 12 25 34 mp2and ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) ∧ ( ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ∧ ( 0 ≤ 𝐶 ∧ 𝐶 < 𝐷 ) ) ) → ( 𝐴 · 𝐶 ) < ( 𝐵 · 𝐷 ) )
36 35 an4s ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ∧ ( 0 ≤ 𝐶 ∧ 𝐶 < 𝐷 ) ) ) → ( 𝐴 · 𝐶 ) < ( 𝐵 · 𝐷 ) )