Metamath Proof Explorer

Theorem lediv2aALT

Description: Division of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion lediv2aALT 
|- ( ( ( 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 gt0ne0 
 |-  ( ( A e. RR /\ 0 < A ) -> A =/= 0 )
5 rereccl 
 |-  ( ( A e. RR /\ A =/= 0 ) -> ( 1 / A ) e. RR )
6 4 5 syldan 
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 / A ) e. RR )
7 3 6 anim12i 
 |-  ( ( ( B e. RR /\ 0 < B ) /\ ( A e. RR /\ 0 < A ) ) -> ( ( 1 / B ) e. RR /\ ( 1 / A ) e. RR ) )
8 7 ancoms 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( 1 / B ) e. RR /\ ( 1 / A ) e. RR ) )
9 8 3adant3 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 <_ C ) ) -> ( ( 1 / B ) e. RR /\ ( 1 / A ) e. RR ) )
10 simp3 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 <_ C ) ) -> ( C e. RR /\ 0 <_ C ) )
11 df-3an 
 |-  ( ( ( 1 / B ) e. RR /\ ( 1 / A ) e. RR /\ ( C e. RR /\ 0 <_ C ) ) <-> ( ( ( 1 / B ) e. RR /\ ( 1 / A ) e. RR ) /\ ( C e. RR /\ 0 <_ C ) ) )
12 9 10 11 sylanbrc 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 <_ C ) ) -> ( ( 1 / B ) e. RR /\ ( 1 / A ) e. RR /\ ( C e. RR /\ 0 <_ C ) ) )
13 lemul2a 
 |-  ( ( ( ( 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 ) ) )
14 13 ex 
 |-  ( ( ( 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 ) ) ) )
15 12 14 syl 
 |-  ( ( ( 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 ) ) ) )
16 lerec 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A <_ B <-> ( 1 / B ) <_ ( 1 / A ) ) )
17 16 3adant3 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 <_ C ) ) -> ( A <_ B <-> ( 1 / B ) <_ ( 1 / A ) ) )
18 recn 
 |-  ( C e. RR -> C e. CC )
19 18 adantr 
 |-  ( ( C e. RR /\ 0 <_ C ) -> C e. CC )
20 recn 
 |-  ( B e. RR -> B e. CC )
21 20 adantr 
 |-  ( ( B e. RR /\ 0 < B ) -> B e. CC )
22 21 1 jca 
 |-  ( ( B e. RR /\ 0 < B ) -> ( B e. CC /\ B =/= 0 ) )
23 19 22 anim12i 
 |-  ( ( ( C e. RR /\ 0 <_ C ) /\ ( B e. RR /\ 0 < B ) ) -> ( C e. CC /\ ( B e. CC /\ B =/= 0 ) ) )
24 3anass 
 |-  ( ( C e. CC /\ B e. CC /\ B =/= 0 ) <-> ( C e. CC /\ ( B e. CC /\ B =/= 0 ) ) )
25 23 24 sylibr 
 |-  ( ( ( C e. RR /\ 0 <_ C ) /\ ( B e. RR /\ 0 < B ) ) -> ( C e. CC /\ B e. CC /\ B =/= 0 ) )
26 divrec 
 |-  ( ( C e. CC /\ B e. CC /\ B =/= 0 ) -> ( C / B ) = ( C x. ( 1 / B ) ) )
27 25 26 syl 
 |-  ( ( ( C e. RR /\ 0 <_ C ) /\ ( B e. RR /\ 0 < B ) ) -> ( C / B ) = ( C x. ( 1 / B ) ) )
28 27 ancoms 
 |-  ( ( ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 <_ C ) ) -> ( C / B ) = ( C x. ( 1 / B ) ) )
29 28 3adant1 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 <_ C ) ) -> ( C / B ) = ( C x. ( 1 / B ) ) )
30 recn 
 |-  ( A e. RR -> A e. CC )
31 30 adantr 
 |-  ( ( A e. RR /\ 0 < A ) -> A e. CC )
32 31 4 jca 
 |-  ( ( A e. RR /\ 0 < A ) -> ( A e. CC /\ A =/= 0 ) )
33 19 32 anim12i 
 |-  ( ( ( C e. RR /\ 0 <_ C ) /\ ( A e. RR /\ 0 < A ) ) -> ( C e. CC /\ ( A e. CC /\ A =/= 0 ) ) )
34 3anass 
 |-  ( ( C e. CC /\ A e. CC /\ A =/= 0 ) <-> ( C e. CC /\ ( A e. CC /\ A =/= 0 ) ) )
35 33 34 sylibr 
 |-  ( ( ( C e. RR /\ 0 <_ C ) /\ ( A e. RR /\ 0 < A ) ) -> ( C e. CC /\ A e. CC /\ A =/= 0 ) )
36 divrec 
 |-  ( ( C e. CC /\ A e. CC /\ A =/= 0 ) -> ( C / A ) = ( C x. ( 1 / A ) ) )
37 35 36 syl 
 |-  ( ( ( C e. RR /\ 0 <_ C ) /\ ( A e. RR /\ 0 < A ) ) -> ( C / A ) = ( C x. ( 1 / A ) ) )
38 37 ancoms 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( C e. RR /\ 0 <_ C ) ) -> ( C / A ) = ( C x. ( 1 / A ) ) )
39 38 3adant2 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 <_ C ) ) -> ( C / A ) = ( C x. ( 1 / A ) ) )
40 29 39 breq12d 
 |-  ( ( ( 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 ) ) ) )
41 15 17 40 3imtr4d 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 <_ C ) ) -> ( A <_ B -> ( C / B ) <_ ( C / A ) ) )