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 ) ) )