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 | ⊢ ( 𝜑 → 𝐴 ∈ ℝ ) | |
ltmul1d.2 | ⊢ ( 𝜑 → 𝐵 ∈ ℝ ) | ||
ltmul1d.3 | ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ ) | ||
Assertion | lemul1d | ⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltmul1d.1 | ⊢ ( 𝜑 → 𝐴 ∈ ℝ ) | |
2 | ltmul1d.2 | ⊢ ( 𝜑 → 𝐵 ∈ ℝ ) | |
3 | ltmul1d.3 | ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ ) | |
4 | 3 | rpregt0d | ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) |
5 | lemul1 | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) ) | |
6 | 1 2 4 5 | syl3anc | ⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 · 𝐶 ) ≤ ( 𝐵 · 𝐶 ) ) ) |