This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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