# Metamath Proof Explorer

## Theorem ltmuldiv2

Description: 'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004)

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

### Proof

Step Hyp Ref Expression
1 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
2 recn ${⊢}{C}\in ℝ\to {C}\in ℂ$
3 mulcom ${⊢}\left({A}\in ℂ\wedge {C}\in ℂ\right)\to {A}{C}={C}{A}$
4 1 2 3 syl2an ${⊢}\left({A}\in ℝ\wedge {C}\in ℝ\right)\to {A}{C}={C}{A}$
5 4 adantrr ${⊢}\left({A}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to {A}{C}={C}{A}$
6 5 3adant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to {A}{C}={C}{A}$
7 6 breq1d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}{C}<{B}↔{C}{A}<{B}\right)$
8 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)$
9 7 8 bitr3d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({C}{A}<{B}↔{A}<\frac{{B}}{{C}}\right)$