Metamath Proof Explorer


Theorem ltdiv23d

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

Proof

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