This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ → A ∈ ℝ
ltdiv23d.2 ⊢ φ → B ∈ ℝ +
ltdiv23d.3 ⊢ φ → C ∈ ℝ +
ltdiv23d.4 ⊢ φ → A B < C
Assertion ltdiv23d ⊢ φ → A C < B

Proof

Step Hyp Ref Expression
1 ltdiv23d.1 ⊢ φ → A ∈ ℝ
2 ltdiv23d.2 ⊢ φ → B ∈ ℝ +
3 ltdiv23d.3 ⊢ φ → C ∈ ℝ +
4 ltdiv23d.4 ⊢ φ → A B < C
5 2 rpregt0d ⊢ φ → B ∈ ℝ ∧ 0 < B
6 3 rpregt0d ⊢ φ → C ∈ ℝ ∧ 0 < C
7 ltdiv23 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < B ∧ C ∈ ℝ ∧ 0 < C → A B < C ↔ A C < B
8 1 5 6 7 syl3anc ⊢ φ → A B < C ↔ A C < B
9 4 8 mpbid ⊢ φ → A C < B