Metamath Proof Explorer


Theorem ltdiv23i

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 < 𝐶 ) → ( ( 𝐴 / 𝐵 ) < 𝐶 ↔ ( 𝐴 / 𝐶 ) < 𝐵 ) )

Proof

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 < 𝐶 ) → ( ( 𝐴 / 𝐵 ) < 𝐶 ↔ ( 𝐴 / 𝐶 ) < 𝐵 ) )