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

Metamath Proof Explorer

Theorem ltmul12ad

Description: Comparison of product of two positive 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 )
ltmul12ad.4 
|- ( ph -> 0 <_ A )
ltmul12ad.5 
|- ( ph -> A < B )
ltmul12ad.6 
|- ( ph -> 0 <_ C )
ltmul12ad.7 
|- ( ph -> C < D )
Assertion ltmul12ad 
|- ( 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 ltmul12ad.4 
 |-  ( ph -> 0 <_ A )
6 ltmul12ad.5 
 |-  ( ph -> A < B )
7 ltmul12ad.6 
 |-  ( ph -> 0 <_ C )
8 ltmul12ad.7 
 |-  ( ph -> C < D )
9 1 2 jca 
 |-  ( ph -> ( A e. RR /\ B e. RR ) )
10 5 6 jca 
 |-  ( ph -> ( 0 <_ A /\ A < B ) )
11 3 4 jca 
 |-  ( ph -> ( C e. RR /\ D e. RR ) )
12 7 8 jca 
 |-  ( ph -> ( 0 <_ C /\ C < D ) )
13 ltmul12a 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 <_ C /\ C < D ) ) ) -> ( A x. C ) < ( B x. D ) )
14 9 10 11 12 13 syl22anc 
 |-  ( ph -> ( A x. C ) < ( B x. D ) )