Description: The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ltmul1d.1 | ⊢ ( 𝜑 → 𝐴 ∈ ℝ ) | |
ltmul1d.2 | ⊢ ( 𝜑 → 𝐵 ∈ ℝ ) | ||
ltmul1d.3 | ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ ) | ||
Assertion | ltmul1d | ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ ( 𝐴 · 𝐶 ) < ( 𝐵 · 𝐶 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltmul1d.1 | ⊢ ( 𝜑 → 𝐴 ∈ ℝ ) | |
2 | ltmul1d.2 | ⊢ ( 𝜑 → 𝐵 ∈ ℝ ) | |
3 | ltmul1d.3 | ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ ) | |
4 | 3 | rpregt0d | ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) |
5 | ltmul1 | ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 · 𝐶 ) < ( 𝐵 · 𝐶 ) ) ) | |
6 | 1 2 4 5 | syl3anc | ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ ( 𝐴 · 𝐶 ) < ( 𝐵 · 𝐶 ) ) ) |