Metamath Proof Explorer

Theorem ltdiv1

Description: Division of both sides of 'less than' by a positive number. (Contributed by NM, 10-Oct-2004) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> A e. RR )
2 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> B e. RR )
3 simp3l 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> C e. RR )
4 simp3r 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> 0 < C )
5 4 gt0ne0d 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> C =/= 0 )
6 3 5 rereccld 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( 1 / C ) e. RR )
7 recgt0 
 |-  ( ( C e. RR /\ 0 < C ) -> 0 < ( 1 / C ) )
8 7 3ad2ant3 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> 0 < ( 1 / C ) )
9 ltmul1 
 |-  ( ( A e. RR /\ B e. RR /\ ( ( 1 / C ) e. RR /\ 0 < ( 1 / C ) ) ) -> ( A < B <-> ( A x. ( 1 / C ) ) < ( B x. ( 1 / C ) ) ) )
10 1 2 6 8 9 syl112anc 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( A x. ( 1 / C ) ) < ( B x. ( 1 / C ) ) ) )
11 1 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> A e. CC )
12 3 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> C e. CC )
13 11 12 5 divrecd 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A / C ) = ( A x. ( 1 / C ) ) )
14 2 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> B e. CC )
15 14 12 5 divrecd 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( B / C ) = ( B x. ( 1 / C ) ) )
16 13 15 breq12d 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) < ( B / C ) <-> ( A x. ( 1 / C ) ) < ( B x. ( 1 / C ) ) ) )
17 10 16 bitr4d 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( A / C ) < ( B / C ) ) )