Metamath Proof Explorer


Theorem lemul12ad

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

Ref Expression
Hypotheses ltp1d.1
|- ( ph -> A e. RR )
divgt0d.2
|- ( ph -> B e. RR )
lemul1ad.3
|- ( ph -> C e. RR )
ltmul12ad.3
|- ( ph -> D e. RR )
lemul12ad.4
|- ( ph -> 0 <_ A )
lemul12ad.5
|- ( ph -> 0 <_ C )
lemul12ad.6
|- ( ph -> A <_ B )
lemul12ad.7
|- ( ph -> C <_ D )
Assertion lemul12ad
|- ( ph -> ( A x. C ) <_ ( B x. D ) )

Proof

Step Hyp Ref Expression
1 ltp1d.1
 |-  ( ph -> A e. RR )
2 divgt0d.2
 |-  ( ph -> B e. RR )
3 lemul1ad.3
 |-  ( ph -> C e. RR )
4 ltmul12ad.3
 |-  ( ph -> D e. RR )
5 lemul12ad.4
 |-  ( ph -> 0 <_ A )
6 lemul12ad.5
 |-  ( ph -> 0 <_ C )
7 lemul12ad.6
 |-  ( ph -> A <_ B )
8 lemul12ad.7
 |-  ( ph -> C <_ D )
9 1 5 jca
 |-  ( ph -> ( A e. RR /\ 0 <_ A ) )
10 3 6 jca
 |-  ( ph -> ( C e. RR /\ 0 <_ C ) )
11 lemul12a
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR ) /\ ( ( C e. RR /\ 0 <_ C ) /\ D e. RR ) ) -> ( ( A <_ B /\ C <_ D ) -> ( A x. C ) <_ ( B x. D ) ) )
12 9 2 10 4 11 syl22anc
 |-  ( ph -> ( ( A <_ B /\ C <_ D ) -> ( A x. C ) <_ ( B x. D ) ) )
13 7 8 12 mp2and
 |-  ( ph -> ( A x. C ) <_ ( B x. D ) )