# Metamath Proof Explorer

## Theorem lt2mul2div

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

Ref Expression
Assertion lt2mul2div ${⊢}\left(\left({A}\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\wedge \left({C}\in ℝ\wedge \left({D}\in ℝ\wedge 0<{D}\right)\right)\right)\to \left({A}{B}<{C}{D}↔\frac{{A}}{{D}}<\frac{{C}}{{B}}\right)$

### Proof

Step Hyp Ref Expression
1 recn ${⊢}{C}\in ℝ\to {C}\in ℂ$
2 recn ${⊢}{D}\in ℝ\to {D}\in ℂ$
3 mulcom ${⊢}\left({C}\in ℂ\wedge {D}\in ℂ\right)\to {C}{D}={D}{C}$
4 1 2 3 syl2an ${⊢}\left({C}\in ℝ\wedge {D}\in ℝ\right)\to {C}{D}={D}{C}$
5 4 oveq1d ${⊢}\left({C}\in ℝ\wedge {D}\in ℝ\right)\to \frac{{C}{D}}{{B}}=\frac{{D}{C}}{{B}}$
6 5 adantl ${⊢}\left(\left({B}\in ℝ\wedge 0<{B}\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\to \frac{{C}{D}}{{B}}=\frac{{D}{C}}{{B}}$
7 2 ad2antll ${⊢}\left(\left({B}\in ℝ\wedge 0<{B}\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\to {D}\in ℂ$
8 1 ad2antrl ${⊢}\left(\left({B}\in ℝ\wedge 0<{B}\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\to {C}\in ℂ$
9 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
10 9 adantr ${⊢}\left({B}\in ℝ\wedge 0<{B}\right)\to {B}\in ℂ$
11 gt0ne0 ${⊢}\left({B}\in ℝ\wedge 0<{B}\right)\to {B}\ne 0$
12 10 11 jca ${⊢}\left({B}\in ℝ\wedge 0<{B}\right)\to \left({B}\in ℂ\wedge {B}\ne 0\right)$
13 12 adantr ${⊢}\left(\left({B}\in ℝ\wedge 0<{B}\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\to \left({B}\in ℂ\wedge {B}\ne 0\right)$
14 divass ${⊢}\left({D}\in ℂ\wedge {C}\in ℂ\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to \frac{{D}{C}}{{B}}={D}\left(\frac{{C}}{{B}}\right)$
15 7 8 13 14 syl3anc ${⊢}\left(\left({B}\in ℝ\wedge 0<{B}\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\to \frac{{D}{C}}{{B}}={D}\left(\frac{{C}}{{B}}\right)$
16 6 15 eqtrd ${⊢}\left(\left({B}\in ℝ\wedge 0<{B}\right)\wedge \left({C}\in ℝ\wedge {D}\in ℝ\right)\right)\to \frac{{C}{D}}{{B}}={D}\left(\frac{{C}}{{B}}\right)$
17 16 adantrrr ${⊢}\left(\left({B}\in ℝ\wedge 0<{B}\right)\wedge \left({C}\in ℝ\wedge \left({D}\in ℝ\wedge 0<{D}\right)\right)\right)\to \frac{{C}{D}}{{B}}={D}\left(\frac{{C}}{{B}}\right)$
18 17 adantll ${⊢}\left(\left({A}\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\wedge \left({C}\in ℝ\wedge \left({D}\in ℝ\wedge 0<{D}\right)\right)\right)\to \frac{{C}{D}}{{B}}={D}\left(\frac{{C}}{{B}}\right)$
19 18 breq2d ${⊢}\left(\left({A}\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\wedge \left({C}\in ℝ\wedge \left({D}\in ℝ\wedge 0<{D}\right)\right)\right)\to \left({A}<\frac{{C}{D}}{{B}}↔{A}<{D}\left(\frac{{C}}{{B}}\right)\right)$
20 simpll ${⊢}\left(\left({A}\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\wedge \left({C}\in ℝ\wedge \left({D}\in ℝ\wedge 0<{D}\right)\right)\right)\to {A}\in ℝ$
21 remulcl ${⊢}\left({C}\in ℝ\wedge {D}\in ℝ\right)\to {C}{D}\in ℝ$
22 21 adantrr ${⊢}\left({C}\in ℝ\wedge \left({D}\in ℝ\wedge 0<{D}\right)\right)\to {C}{D}\in ℝ$
23 22 adantl ${⊢}\left(\left({A}\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\wedge \left({C}\in ℝ\wedge \left({D}\in ℝ\wedge 0<{D}\right)\right)\right)\to {C}{D}\in ℝ$
24 simplr ${⊢}\left(\left({A}\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\wedge \left({C}\in ℝ\wedge \left({D}\in ℝ\wedge 0<{D}\right)\right)\right)\to \left({B}\in ℝ\wedge 0<{B}\right)$
25 ltmuldiv ${⊢}\left({A}\in ℝ\wedge {C}{D}\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left({A}{B}<{C}{D}↔{A}<\frac{{C}{D}}{{B}}\right)$
26 20 23 24 25 syl3anc ${⊢}\left(\left({A}\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\wedge \left({C}\in ℝ\wedge \left({D}\in ℝ\wedge 0<{D}\right)\right)\right)\to \left({A}{B}<{C}{D}↔{A}<\frac{{C}{D}}{{B}}\right)$
27 simpl ${⊢}\left({B}\in ℝ\wedge 0<{B}\right)\to {B}\in ℝ$
28 27 11 jca ${⊢}\left({B}\in ℝ\wedge 0<{B}\right)\to \left({B}\in ℝ\wedge {B}\ne 0\right)$
29 redivcl ${⊢}\left({C}\in ℝ\wedge {B}\in ℝ\wedge {B}\ne 0\right)\to \frac{{C}}{{B}}\in ℝ$
30 29 3expb ${⊢}\left({C}\in ℝ\wedge \left({B}\in ℝ\wedge {B}\ne 0\right)\right)\to \frac{{C}}{{B}}\in ℝ$
31 28 30 sylan2 ${⊢}\left({C}\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \frac{{C}}{{B}}\in ℝ$
32 31 ancoms ${⊢}\left(\left({B}\in ℝ\wedge 0<{B}\right)\wedge {C}\in ℝ\right)\to \frac{{C}}{{B}}\in ℝ$
33 32 ad2ant2lr ${⊢}\left(\left({A}\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\wedge \left({C}\in ℝ\wedge \left({D}\in ℝ\wedge 0<{D}\right)\right)\right)\to \frac{{C}}{{B}}\in ℝ$
34 simprr ${⊢}\left(\left({A}\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\wedge \left({C}\in ℝ\wedge \left({D}\in ℝ\wedge 0<{D}\right)\right)\right)\to \left({D}\in ℝ\wedge 0<{D}\right)$
35 ltdivmul ${⊢}\left({A}\in ℝ\wedge \frac{{C}}{{B}}\in ℝ\wedge \left({D}\in ℝ\wedge 0<{D}\right)\right)\to \left(\frac{{A}}{{D}}<\frac{{C}}{{B}}↔{A}<{D}\left(\frac{{C}}{{B}}\right)\right)$
36 20 33 34 35 syl3anc ${⊢}\left(\left({A}\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\wedge \left({C}\in ℝ\wedge \left({D}\in ℝ\wedge 0<{D}\right)\right)\right)\to \left(\frac{{A}}{{D}}<\frac{{C}}{{B}}↔{A}<{D}\left(\frac{{C}}{{B}}\right)\right)$
37 19 26 36 3bitr4d ${⊢}\left(\left({A}\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\wedge \left({C}\in ℝ\wedge \left({D}\in ℝ\wedge 0<{D}\right)\right)\right)\to \left({A}{B}<{C}{D}↔\frac{{A}}{{D}}<\frac{{C}}{{B}}\right)$