This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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