Metamath Proof Explorer

Theorem lediv2

Description: Division of a positive number by both sides of 'less than or equal to'. (Contributed by NM, 10-Jan-2006)

Ref Expression
Assertion lediv2 
|- ( ( ( 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 gt0ne0 
 |-  ( ( B e. RR /\ 0 < B ) -> B =/= 0 )
2 rereccl 
 |-  ( ( B e. RR /\ B =/= 0 ) -> ( 1 / B ) e. RR )
3 1 2 syldan 
 |-  ( ( B e. RR /\ 0 < B ) -> ( 1 / B ) e. RR )
4 3 3ad2ant2 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( 1 / B ) e. RR )
5 gt0ne0 
 |-  ( ( A e. RR /\ 0 < A ) -> A =/= 0 )
6 rereccl 
 |-  ( ( A e. RR /\ A =/= 0 ) -> ( 1 / A ) e. RR )
7 5 6 syldan 
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 / A ) e. RR )
8 7 3ad2ant1 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( 1 / A ) e. RR )
9 simp3l 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> C e. RR )
10 simp3r 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> 0 < C )
11 lemul2 
 |-  ( ( ( 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 ) ) ) )
12 4 8 9 10 11 syl112anc 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( 1 / B ) <_ ( 1 / A ) <-> ( C x. ( 1 / B ) ) <_ ( C x. ( 1 / A ) ) ) )
13 lerec 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A <_ B <-> ( 1 / B ) <_ ( 1 / A ) ) )
14 13 3adant3 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> ( 1 / B ) <_ ( 1 / A ) ) )
15 recn 
 |-  ( C e. RR -> C e. CC )
16 recn 
 |-  ( B e. RR -> B e. CC )
17 16 adantr 
 |-  ( ( B e. RR /\ 0 < B ) -> B e. CC )
18 17 1 jca 
 |-  ( ( B e. RR /\ 0 < B ) -> ( B e. CC /\ B =/= 0 ) )
19 divrec 
 |-  ( ( C e. CC /\ B e. CC /\ B =/= 0 ) -> ( C / B ) = ( C x. ( 1 / B ) ) )
20 19 3expb 
 |-  ( ( C e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( C / B ) = ( C x. ( 1 / B ) ) )
21 15 18 20 syl2an 
 |-  ( ( C e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( C / B ) = ( C x. ( 1 / B ) ) )
22 21 3adant2 
 |-  ( ( C e. RR /\ ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( C / B ) = ( C x. ( 1 / B ) ) )
23 recn 
 |-  ( A e. RR -> A e. CC )
24 23 adantr 
 |-  ( ( A e. RR /\ 0 < A ) -> A e. CC )
25 24 5 jca 
 |-  ( ( A e. RR /\ 0 < A ) -> ( A e. CC /\ A =/= 0 ) )
26 divrec 
 |-  ( ( C e. CC /\ A e. CC /\ A =/= 0 ) -> ( C / A ) = ( C x. ( 1 / A ) ) )
27 26 3expb 
 |-  ( ( C e. CC /\ ( A e. CC /\ A =/= 0 ) ) -> ( C / A ) = ( C x. ( 1 / A ) ) )
28 15 25 27 syl2an 
 |-  ( ( C e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( C / A ) = ( C x. ( 1 / A ) ) )
29 28 3adant3 
 |-  ( ( C e. RR /\ ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( C / A ) = ( C x. ( 1 / A ) ) )
30 22 29 breq12d 
 |-  ( ( C e. RR /\ ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( C / B ) <_ ( C / A ) <-> ( C x. ( 1 / B ) ) <_ ( C x. ( 1 / A ) ) ) )
31 30 3coml 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ C e. RR ) -> ( ( C / B ) <_ ( C / A ) <-> ( C x. ( 1 / B ) ) <_ ( C x. ( 1 / A ) ) ) )
32 31 3adant3r 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( C / B ) <_ ( C / A ) <-> ( C x. ( 1 / B ) ) <_ ( C x. ( 1 / A ) ) ) )
33 12 14 32 3bitr4d 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> ( C / B ) <_ ( C / A ) ) )