Metamath Proof Explorer

Theorem ltmul1i

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)

Ref Expression
Hypotheses ltplus1.1 ⊢ A ∈ ℝ
prodgt0.2 ⊢ B ∈ ℝ
ltmul1.3 ⊢ C ∈ ℝ
Assertion ltmul1i ⊢ 0 < C → A < B ↔ A ⁢ C < B ⁢ C

Proof

Step Hyp Ref Expression
1 ltplus1.1 ⊢ A ∈ ℝ
2 prodgt0.2 ⊢ B ∈ ℝ
3 ltmul1.3 ⊢ C ∈ ℝ
4 ltmul1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A < B ↔ A ⁢ C < B ⁢ C
5 1 2 4 mp3an12 ⊢ C ∈ ℝ ∧ 0 < C → A < B ↔ A ⁢ C < B ⁢ C
6 3 5 mpan ⊢ 0 < C → A < B ↔ A ⁢ C < B ⁢ C