Metamath Proof Explorer

Theorem ltdiv2

Description: Division of a positive number by both sides of 'less than'. (Contributed by NM, 27-Apr-2005)

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

Proof

Step Hyp Ref Expression
1 ltrec 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A < B <-> ( 1 / B ) < ( 1 / A ) ) )
2 1 3adant3 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( 1 / B ) < ( 1 / A ) ) )
3 gt0ne0 
 |-  ( ( B e. RR /\ 0 < B ) -> B =/= 0 )
4 rereccl 
 |-  ( ( B e. RR /\ B =/= 0 ) -> ( 1 / B ) e. RR )
5 3 4 syldan 
 |-  ( ( B e. RR /\ 0 < B ) -> ( 1 / B ) e. RR )
6 gt0ne0 
 |-  ( ( A e. RR /\ 0 < A ) -> A =/= 0 )
7 rereccl 
 |-  ( ( A e. RR /\ A =/= 0 ) -> ( 1 / A ) e. RR )
8 6 7 syldan 
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 / A ) e. RR )
9 ltmul2 
 |-  ( ( ( 1 / B ) e. RR /\ ( 1 / A ) e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( 1 / B ) < ( 1 / A ) <-> ( C x. ( 1 / B ) ) < ( C x. ( 1 / A ) ) ) )
10 8 9 syl3an2 
 |-  ( ( ( 1 / B ) e. RR /\ ( A e. RR /\ 0 < A ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( 1 / B ) < ( 1 / A ) <-> ( C x. ( 1 / B ) ) < ( C x. ( 1 / A ) ) ) )
11 5 10 syl3an1 
 |-  ( ( ( B e. RR /\ 0 < B ) /\ ( A e. RR /\ 0 < A ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( 1 / B ) < ( 1 / A ) <-> ( C x. ( 1 / B ) ) < ( C x. ( 1 / A ) ) ) )
12 recn 
 |-  ( C e. RR -> C e. CC )
13 12 adantr 
 |-  ( ( C e. RR /\ 0 < C ) -> C e. CC )
14 recn 
 |-  ( B e. RR -> B e. CC )
15 14 adantr 
 |-  ( ( B e. RR /\ 0 < B ) -> B e. CC )
16 15 3 jca 
 |-  ( ( B e. RR /\ 0 < B ) -> ( B e. CC /\ B =/= 0 ) )
17 recn 
 |-  ( A e. RR -> A e. CC )
18 17 adantr 
 |-  ( ( A e. RR /\ 0 < A ) -> A e. CC )
19 18 6 jca 
 |-  ( ( A e. RR /\ 0 < A ) -> ( A e. CC /\ A =/= 0 ) )
20 divrec 
 |-  ( ( C e. CC /\ B e. CC /\ B =/= 0 ) -> ( C / B ) = ( C x. ( 1 / B ) ) )
21 20 3expb 
 |-  ( ( C e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( C / B ) = ( C x. ( 1 / B ) ) )
22 21 3adant3 
 |-  ( ( C e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( A e. CC /\ A =/= 0 ) ) -> ( C / B ) = ( C x. ( 1 / B ) ) )
23 divrec 
 |-  ( ( C e. CC /\ A e. CC /\ A =/= 0 ) -> ( C / A ) = ( C x. ( 1 / A ) ) )
24 23 3expb 
 |-  ( ( C e. CC /\ ( A e. CC /\ A =/= 0 ) ) -> ( C / A ) = ( C x. ( 1 / A ) ) )
25 24 3adant2 
 |-  ( ( C e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( A e. CC /\ A =/= 0 ) ) -> ( C / A ) = ( C x. ( 1 / A ) ) )
26 22 25 breq12d 
 |-  ( ( C e. CC /\ ( B e. CC /\ B =/= 0 ) /\ ( A e. CC /\ A =/= 0 ) ) -> ( ( C / B ) < ( C / A ) <-> ( C x. ( 1 / B ) ) < ( C x. ( 1 / A ) ) ) )
27 13 16 19 26 syl3an 
 |-  ( ( ( C e. RR /\ 0 < C ) /\ ( B e. RR /\ 0 < B ) /\ ( A e. RR /\ 0 < A ) ) -> ( ( C / B ) < ( C / A ) <-> ( C x. ( 1 / B ) ) < ( C x. ( 1 / A ) ) ) )
28 27 3coml 
 |-  ( ( ( B e. RR /\ 0 < B ) /\ ( A e. RR /\ 0 < A ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( C / B ) < ( C / A ) <-> ( C x. ( 1 / B ) ) < ( C x. ( 1 / A ) ) ) )
29 11 28 bitr4d 
 |-  ( ( ( B e. RR /\ 0 < B ) /\ ( A e. RR /\ 0 < A ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( 1 / B ) < ( 1 / A ) <-> ( C / B ) < ( C / A ) ) )
30 29 3com12 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( 1 / B ) < ( 1 / A ) <-> ( C / B ) < ( C / A ) ) )
31 2 30 bitrd 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( C / B ) < ( C / A ) ) )