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

Metamath Proof Explorer

Theorem lt2mul2div

Description: 'Less than' relationship between division and multiplication. (Contributed by NM, 8-Jan-2006)

Ref Expression
Assertion lt2mul2div ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( ( 𝐴 · 𝐵 ) < ( 𝐶 · 𝐷 ) ↔ ( 𝐴 / 𝐷 ) < ( 𝐶 / 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 recn ⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
2 recn ⊢ ( 𝐷 ∈ ℝ → 𝐷 ∈ ℂ )
3 mulcom ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐶 · 𝐷 ) = ( 𝐷 · 𝐶 ) )
4 1 2 3 syl2an ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 𝐶 · 𝐷 ) = ( 𝐷 · 𝐶 ) )
5 4 oveq1d ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( 𝐶 · 𝐷 ) / 𝐵 ) = ( ( 𝐷 · 𝐶 ) / 𝐵 ) )
6 5 adantl ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐶 · 𝐷 ) / 𝐵 ) = ( ( 𝐷 · 𝐶 ) / 𝐵 ) )
7 2 ad2antll ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐷 ∈ ℂ )
8 1 ad2antrl ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐶 ∈ ℂ )
9 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
10 9 adantr ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → 𝐵 ∈ ℂ )
11 gt0ne0 ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → 𝐵 ≠ 0 )
12 10 11 jca ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
13 12 adantr ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
14 divass ⊢ ( ( 𝐷 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐷 · 𝐶 ) / 𝐵 ) = ( 𝐷 · ( 𝐶 / 𝐵 ) ) )
15 7 8 13 14 syl3anc ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐷 · 𝐶 ) / 𝐵 ) = ( 𝐷 · ( 𝐶 / 𝐵 ) ) )
16 6 15 eqtrd ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐶 · 𝐷 ) / 𝐵 ) = ( 𝐷 · ( 𝐶 / 𝐵 ) ) )
17 16 adantrrr ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( ( 𝐶 · 𝐷 ) / 𝐵 ) = ( 𝐷 · ( 𝐶 / 𝐵 ) ) )
18 17 adantll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( ( 𝐶 · 𝐷 ) / 𝐵 ) = ( 𝐷 · ( 𝐶 / 𝐵 ) ) )
19 18 breq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( 𝐴 < ( ( 𝐶 · 𝐷 ) / 𝐵 ) ↔ 𝐴 < ( 𝐷 · ( 𝐶 / 𝐵 ) ) ) )
20 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → 𝐴 ∈ ℝ )
21 remulcl ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 𝐶 · 𝐷 ) ∈ ℝ )
22 21 adantrr ⊢ ( ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) → ( 𝐶 · 𝐷 ) ∈ ℝ )
23 22 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( 𝐶 · 𝐷 ) ∈ ℝ )
24 simplr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
25 ltmuldiv ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 · 𝐷 ) ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐴 · 𝐵 ) < ( 𝐶 · 𝐷 ) ↔ 𝐴 < ( ( 𝐶 · 𝐷 ) / 𝐵 ) ) )
26 20 23 24 25 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( ( 𝐴 · 𝐵 ) < ( 𝐶 · 𝐷 ) ↔ 𝐴 < ( ( 𝐶 · 𝐷 ) / 𝐵 ) ) )
27 simpl ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → 𝐵 ∈ ℝ )
28 27 11 jca ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) → ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) )
29 redivcl ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐶 / 𝐵 ) ∈ ℝ )
30 29 3expb ⊢ ( ( 𝐶 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ) → ( 𝐶 / 𝐵 ) ∈ ℝ )
31 28 30 sylan2 ⊢ ( ( 𝐶 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐶 / 𝐵 ) ∈ ℝ )
32 31 ancoms ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ 𝐶 ∈ ℝ ) → ( 𝐶 / 𝐵 ) ∈ ℝ )
33 32 ad2ant2lr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( 𝐶 / 𝐵 ) ∈ ℝ )
34 simprr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) )
35 ltdivmul ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 / 𝐵 ) ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) → ( ( 𝐴 / 𝐷 ) < ( 𝐶 / 𝐵 ) ↔ 𝐴 < ( 𝐷 · ( 𝐶 / 𝐵 ) ) ) )
36 20 33 34 35 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( ( 𝐴 / 𝐷 ) < ( 𝐶 / 𝐵 ) ↔ 𝐴 < ( 𝐷 · ( 𝐶 / 𝐵 ) ) ) )
37 19 26 36 3bitr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) ∧ ( 𝐶 ∈ ℝ ∧ ( 𝐷 ∈ ℝ ∧ 0 < 𝐷 ) ) ) → ( ( 𝐴 · 𝐵 ) < ( 𝐶 · 𝐷 ) ↔ ( 𝐴 / 𝐷 ) < ( 𝐶 / 𝐵 ) ) )