Metamath Proof Explorer


Theorem ledivmul

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

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

Proof

Step Hyp Ref Expression
1 remulcl
 |-  ( ( C e. RR /\ B e. RR ) -> ( C x. B ) e. RR )
2 1 ancoms
 |-  ( ( B e. RR /\ C e. RR ) -> ( C x. B ) e. RR )
3 2 adantrr
 |-  ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( C x. B ) e. RR )
4 3 3adant1
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( C x. B ) e. RR )
5 lediv1
 |-  ( ( A e. RR /\ ( C x. B ) e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ ( C x. B ) <-> ( A / C ) <_ ( ( C x. B ) / C ) ) )
6 4 5 syld3an2
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ ( C x. B ) <-> ( A / C ) <_ ( ( C x. B ) / C ) ) )
7 recn
 |-  ( B e. RR -> B e. CC )
8 7 adantr
 |-  ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> B e. CC )
9 recn
 |-  ( C e. RR -> C e. CC )
10 9 ad2antrl
 |-  ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> C e. CC )
11 gt0ne0
 |-  ( ( C e. RR /\ 0 < C ) -> C =/= 0 )
12 11 adantl
 |-  ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> C =/= 0 )
13 8 10 12 divcan3d
 |-  ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( C x. B ) / C ) = B )
14 13 3adant1
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( C x. B ) / C ) = B )
15 14 breq2d
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) <_ ( ( C x. B ) / C ) <-> ( A / C ) <_ B ) )
16 6 15 bitr2d
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) <_ B <-> A <_ ( C x. B ) ) )