Metamath Proof Explorer


Theorem ltmul1ii

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
prodgt0.2 B
ltmul1.3 C
ltmul1i.4 0 < C
Assertion ltmul1ii A < B A C < B C

Proof

Step Hyp Ref Expression
1 ltplus1.1 A
2 prodgt0.2 B
3 ltmul1.3 C
4 ltmul1i.4 0 < C
5 1 2 3 ltmul1i 0 < C A < B A C < B C
6 4 5 ax-mp A < B A C < B C