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