Metamath Proof Explorer

Theorem ltdivmul2

Description: 'Less than' relationship between division and multiplication. (Contributed by NM, 24-Feb-2005)

Ref Expression
Assertion ltdivmul2 
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) < B <-> A < ( B x. C ) ) )

Proof

Step Hyp Ref Expression
1 ltdivmul 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) < B <-> A < ( C x. B ) ) )
2 recn 
 |-  ( B e. RR -> B e. CC )
3 recn 
 |-  ( C e. RR -> C e. CC )
4 mulcom 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B x. C ) = ( C x. B ) )
5 2 3 4 syl2an 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B x. C ) = ( C x. B ) )
6 5 adantrr 
 |-  ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( B x. C ) = ( C x. B ) )
7 6 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( B x. C ) = ( C x. B ) )
8 7 breq2d 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < ( B x. C ) <-> A < ( C x. B ) ) )
9 1 8 bitr4d 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) < B <-> A < ( B x. C ) ) )