Description: Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ltdiv23d.1 | ⊢ ( 𝜑 → 𝐴 ∈ ℝ ) | |
ltdiv23d.2 | ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ ) | ||
ltdiv23d.3 | ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ ) | ||
ltdiv23d.4 | ⊢ ( 𝜑 → ( 𝐴 / 𝐵 ) < 𝐶 ) | ||
Assertion | ltdiv23d | ⊢ ( 𝜑 → ( 𝐴 / 𝐶 ) < 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltdiv23d.1 | ⊢ ( 𝜑 → 𝐴 ∈ ℝ ) | |
2 | ltdiv23d.2 | ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ ) | |
3 | ltdiv23d.3 | ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ ) | |
4 | ltdiv23d.4 | ⊢ ( 𝜑 → ( 𝐴 / 𝐵 ) < 𝐶 ) | |
5 | 2 | rpregt0d | ⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) |
6 | 3 | rpregt0d | ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) |
7 | ltdiv23 | ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 / 𝐵 ) < 𝐶 ↔ ( 𝐴 / 𝐶 ) < 𝐵 ) ) | |
8 | 1 5 6 7 | syl3anc | ⊢ ( 𝜑 → ( ( 𝐴 / 𝐵 ) < 𝐶 ↔ ( 𝐴 / 𝐶 ) < 𝐵 ) ) |
9 | 4 8 | mpbid | ⊢ ( 𝜑 → ( 𝐴 / 𝐶 ) < 𝐵 ) |