Description: Multiplication of both sides of 'less than or equal to' by a nonnegative number. (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 ) |
||
| lemul1ad.4 | |- ( ph -> 0 <_ C ) |
||
| lemul1ad.5 | |- ( ph -> A <_ B ) |
||
| Assertion | lemul2ad | |- ( ph -> ( C x. A ) <_ ( C x. B ) ) |
| 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 | lemul1ad.4 | |- ( ph -> 0 <_ C ) |
|
| 5 | lemul1ad.5 | |- ( ph -> A <_ B ) |
|
| 6 | 3 4 | jca | |- ( ph -> ( C e. RR /\ 0 <_ C ) ) |
| 7 | lemul2a | |- ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( C x. A ) <_ ( C x. B ) ) |
|
| 8 | 1 2 6 5 7 | syl31anc | |- ( ph -> ( C x. A ) <_ ( C x. B ) ) |