Metamath Proof Explorer

Theorem lediv2a

Description: Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007)

Ref Expression
Assertion lediv2a 
|- ( ( ( ( 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 pm3.2 
 |-  ( C e. RR -> ( C e. RR -> ( C e. RR /\ C e. RR ) ) )
2 1 pm2.43i 
 |-  ( C e. RR -> ( C e. RR /\ C e. RR ) )
3 2 adantr 
 |-  ( ( C e. RR /\ 0 <_ C ) -> ( C e. RR /\ C e. RR ) )
4 leid 
 |-  ( C e. RR -> C <_ C )
5 4 anim1ci 
 |-  ( ( C e. RR /\ 0 <_ C ) -> ( 0 <_ C /\ C <_ C ) )
6 3 5 jca 
 |-  ( ( C e. RR /\ 0 <_ C ) -> ( ( C e. RR /\ C e. RR ) /\ ( 0 <_ C /\ C <_ C ) ) )
7 6 ad2antlr 
 |-  ( ( ( ( A e. RR /\ 0 < A ) /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( ( C e. RR /\ C e. RR ) /\ ( 0 <_ C /\ C <_ C ) ) )
8 7 3adantl2 
 |-  ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( ( C e. RR /\ C e. RR ) /\ ( 0 <_ C /\ C <_ C ) ) )
9 id 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A e. RR /\ B e. RR ) )
10 9 ad2ant2r 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A e. RR /\ B e. RR ) )
11 10 adantr 
 |-  ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) /\ A <_ B ) -> ( A e. RR /\ B e. RR ) )
12 simplr 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 < A )
13 12 anim1i 
 |-  ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) /\ A <_ B ) -> ( 0 < A /\ A <_ B ) )
14 11 13 jca 
 |-  ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) /\ A <_ B ) -> ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ A <_ B ) ) )
15 14 3adantl3 
 |-  ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ A <_ B ) ) )
16 lediv12a 
 |-  ( ( ( ( C e. RR /\ C e. RR ) /\ ( 0 <_ C /\ C <_ C ) ) /\ ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ A <_ B ) ) ) -> ( C / B ) <_ ( C / A ) )
17 8 15 16 syl2anc 
 |-  ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( C / B ) <_ ( C / A ) )