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