Metamath Proof Explorer

Theorem lemul1i

Description: Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 2-Aug-1999)

Ref Expression
Hypotheses ltplus1.1 ⊢ A ∈ ℝ
prodgt0.2 ⊢ B ∈ ℝ
ltmul1.3 ⊢ C ∈ ℝ
Assertion lemul1i ⊢ 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 lemul1 ⊢ 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