Description: Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ltplus1.1 | ⊢ 𝐴 ∈ ℝ | |
prodgt0.2 | ⊢ 𝐵 ∈ ℝ | ||
ltmul1.3 | ⊢ 𝐶 ∈ ℝ | ||
Assertion | ltdiv23i | ⊢ ( ( 0 < 𝐵 ∧ 0 < 𝐶 ) → ( ( 𝐴 / 𝐵 ) < 𝐶 ↔ ( 𝐴 / 𝐶 ) < 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltplus1.1 | ⊢ 𝐴 ∈ ℝ | |
2 | prodgt0.2 | ⊢ 𝐵 ∈ ℝ | |
3 | ltmul1.3 | ⊢ 𝐶 ∈ ℝ | |
4 | ltdiv23 | ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 / 𝐵 ) < 𝐶 ↔ ( 𝐴 / 𝐶 ) < 𝐵 ) ) | |
5 | 1 4 | mp3an1 | ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 / 𝐵 ) < 𝐶 ↔ ( 𝐴 / 𝐶 ) < 𝐵 ) ) |
6 | 2 5 | mpanl1 | ⊢ ( ( 0 < 𝐵 ∧ ( 𝐶 ∈ ℝ ∧ 0 < 𝐶 ) ) → ( ( 𝐴 / 𝐵 ) < 𝐶 ↔ ( 𝐴 / 𝐶 ) < 𝐵 ) ) |
7 | 3 6 | mpanr1 | ⊢ ( ( 0 < 𝐵 ∧ 0 < 𝐶 ) → ( ( 𝐴 / 𝐵 ) < 𝐶 ↔ ( 𝐴 / 𝐶 ) < 𝐵 ) ) |