This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lemul1d

Description: Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses ltmul1d.1 ⊢ φ → A ∈ ℝ
ltmul1d.2 ⊢ φ → B ∈ ℝ
ltmul1d.3 ⊢ φ → C ∈ ℝ +
Assertion lemul1d ⊢ φ → A ≤ B ↔ A ⁢ C ≤ B ⁢ C

Proof

Step Hyp Ref Expression
1 ltmul1d.1 ⊢ φ → A ∈ ℝ
2 ltmul1d.2 ⊢ φ → B ∈ ℝ
3 ltmul1d.3 ⊢ φ → C ∈ ℝ +
4 3 rpregt0d ⊢ φ → C ∈ ℝ ∧ 0 < C
5 lemul1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ≤ B ↔ A ⁢ C ≤ B ⁢ C
6 1 2 4 5 syl3anc ⊢ φ → A ≤ B ↔ A ⁢ C ≤ B ⁢ C