Metamath Proof Explorer

Theorem ledivmul2

Description: 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005)

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

Proof

Step Hyp Ref Expression
1 ledivmul 
 |-  ( ( 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 ) ) )