Description: Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of Apostol p. 20. (Contributed by NM, 16-May-1999) (Proof shortened by Paul Chapman, 25-Jan-2008)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ltplus1.1 | |- A e. RR |
|
| prodgt0.2 | |- B e. RR |
||
| ltmul1.3 | |- C e. RR |
||
| ltmul1i.4 | |- 0 < C |
||
| Assertion | ltmul1ii | |- ( A < B <-> ( A x. C ) < ( B x. C ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ltplus1.1 | |- A e. RR |
|
| 2 | prodgt0.2 | |- B e. RR |
|
| 3 | ltmul1.3 | |- C e. RR |
|
| 4 | ltmul1i.4 | |- 0 < C |
|
| 5 | 1 2 3 | ltmul1i | |- ( 0 < C -> ( A < B <-> ( A x. C ) < ( B x. C ) ) ) |
| 6 | 4 5 | ax-mp | |- ( A < B <-> ( A x. C ) < ( B x. C ) ) |