Metamath Proof Explorer

Theorem lt2mul2div

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

Ref Expression
Assertion lt2mul2div ⊢A∈ℝ∧B∈ℝ∧0<B∧C∈ℝ∧D∈ℝ∧0<D→A⁢B<C⁢D↔AD<CB

Proof

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