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<BAC<BC

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<CA<BAC<BC
6 4 5 ax-mp A<BAC<BC