Metamath Proof Explorer

Theorem lediv1

Description: Division of both sides of a less than or equal to relation by a positive number. (Contributed by NM, 18-Nov-2004)

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

Proof

Step Hyp Ref Expression
1 ltdiv1 
 |-  ( ( B e. RR /\ A e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( B < A <-> ( B / C ) < ( A / C ) ) )
2 1 3com12 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( B < A <-> ( B / C ) < ( A / C ) ) )
3 2 notbid 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( -. B < A <-> -. ( B / C ) < ( A / C ) ) )
4 lenlt 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
5 4 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> -. B < A ) )
6 gt0ne0 
 |-  ( ( C e. RR /\ 0 < C ) -> C =/= 0 )
7 6 3adant1 
 |-  ( ( A e. RR /\ C e. RR /\ 0 < C ) -> C =/= 0 )
8 redivcl 
 |-  ( ( A e. RR /\ C e. RR /\ C =/= 0 ) -> ( A / C ) e. RR )
9 7 8 syld3an3 
 |-  ( ( A e. RR /\ C e. RR /\ 0 < C ) -> ( A / C ) e. RR )
10 9 3expb 
 |-  ( ( A e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A / C ) e. RR )
11 10 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A / C ) e. RR )
12 6 3adant1 
 |-  ( ( B e. RR /\ C e. RR /\ 0 < C ) -> C =/= 0 )
13 redivcl 
 |-  ( ( B e. RR /\ C e. RR /\ C =/= 0 ) -> ( B / C ) e. RR )
14 12 13 syld3an3 
 |-  ( ( B e. RR /\ C e. RR /\ 0 < C ) -> ( B / C ) e. RR )
15 14 3expb 
 |-  ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( B / C ) e. RR )
16 15 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( B / C ) e. RR )
17 11 16 lenltd 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) <_ ( B / C ) <-> -. ( B / C ) < ( A / C ) ) )
18 3 5 17 3bitr4d 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> ( A / C ) <_ ( B / C ) ) )