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
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) < B <-> A < ( B / C ) ) )

Proof

Step Hyp Ref Expression
1 simp1
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> A e. RR )
2 simp3l
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> C e. RR )
3 1 2 remulcld
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A x. C ) e. RR )
4 ltdiv1
 |-  ( ( ( A x. C ) e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) < B <-> ( ( A x. C ) / C ) < ( B / C ) ) )
5 3 4 syld3an1
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) < B <-> ( ( A x. C ) / C ) < ( B / C ) ) )
6 1 recnd
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> A e. CC )
7 2 recnd
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> C e. CC )
8 simp3r
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> 0 < C )
9 8 gt0ne0d
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> C =/= 0 )
10 6 7 9 divcan4d
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) / C ) = A )
11 10 breq1d
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( ( A x. C ) / C ) < ( B / C ) <-> A < ( B / C ) ) )
12 5 11 bitrd
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) < B <-> A < ( B / C ) ) )