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 ) )