# Metamath Proof Explorer

## Theorem ltmuldiv

Description: 'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

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

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to {A}\in ℝ$
2 simp3l ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to {C}\in ℝ$
3 1 2 remulcld ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to {A}{C}\in ℝ$
4 ltdiv1 ${⊢}\left({A}{C}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}{C}<{B}↔\frac{{A}{C}}{{C}}<\frac{{B}}{{C}}\right)$
5 3 4 syld3an1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}{C}<{B}↔\frac{{A}{C}}{{C}}<\frac{{B}}{{C}}\right)$
6 1 recnd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to {A}\in ℂ$
7 2 recnd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to {C}\in ℂ$
8 simp3r ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to 0<{C}$
9 8 gt0ne0d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to {C}\ne 0$
10 6 7 9 divcan4d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \frac{{A}{C}}{{C}}={A}$
11 10 breq1d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left(\frac{{A}{C}}{{C}}<\frac{{B}}{{C}}↔{A}<\frac{{B}}{{C}}\right)$
12 5 11 bitrd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}{C}<{B}↔{A}<\frac{{B}}{{C}}\right)$