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 𝐴 ∈ ℝ
prodgt0.2 𝐵 ∈ ℝ
ltmul1.3 𝐶 ∈ ℝ
ltmul1i.4 0 < 𝐶
Assertion ltmul1ii ( 𝐴 < 𝐵 ↔ ( 𝐴 · 𝐶 ) < ( 𝐵 · 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ltplus1.1 𝐴 ∈ ℝ
2 prodgt0.2 𝐵 ∈ ℝ
3 ltmul1.3 𝐶 ∈ ℝ
4 ltmul1i.4 0 < 𝐶
5 1 2 3 ltmul1i ( 0 < 𝐶 → ( 𝐴 < 𝐵 ↔ ( 𝐴 · 𝐶 ) < ( 𝐵 · 𝐶 ) ) )
6 4 5 ax-mp ( 𝐴 < 𝐵 ↔ ( 𝐴 · 𝐶 ) < ( 𝐵 · 𝐶 ) )