Metamath Proof Explorer


Theorem lediv12ad

Description: Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses ltmul1d.1
|- ( ph -> A e. RR )
ltmul1d.2
|- ( ph -> B e. RR )
ltmul1d.3
|- ( ph -> C e. RR+ )
lediv12ad.4
|- ( ph -> D e. RR )
lediv12ad.5
|- ( ph -> 0 <_ A )
lediv12ad.6
|- ( ph -> A <_ B )
lediv12ad.7
|- ( ph -> C <_ D )
Assertion lediv12ad
|- ( ph -> ( A / D ) <_ ( B / C ) )

Proof

Step Hyp Ref Expression
1 ltmul1d.1
 |-  ( ph -> A e. RR )
2 ltmul1d.2
 |-  ( ph -> B e. RR )
3 ltmul1d.3
 |-  ( ph -> C e. RR+ )
4 lediv12ad.4
 |-  ( ph -> D e. RR )
5 lediv12ad.5
 |-  ( ph -> 0 <_ A )
6 lediv12ad.6
 |-  ( ph -> A <_ B )
7 lediv12ad.7
 |-  ( ph -> C <_ D )
8 1 2 jca
 |-  ( ph -> ( A e. RR /\ B e. RR ) )
9 5 6 jca
 |-  ( ph -> ( 0 <_ A /\ A <_ B ) )
10 3 rpred
 |-  ( ph -> C e. RR )
11 10 4 jca
 |-  ( ph -> ( C e. RR /\ D e. RR ) )
12 3 rpgt0d
 |-  ( ph -> 0 < C )
13 12 7 jca
 |-  ( ph -> ( 0 < C /\ C <_ D ) )
14 lediv12a
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) ) -> ( A / D ) <_ ( B / C ) )
15 8 9 11 13 14 syl22anc
 |-  ( ph -> ( A / D ) <_ ( B / C ) )