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

Metamath Proof Explorer

Theorem ltdiv2dd

Description: Division of a positive number by both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses ltdiv2dd.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
ltdiv2dd.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
ltdiv2dd.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
ltdiv2dd.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
Assertion ltdiv2dd ( 𝜑 → ( 𝐶 / 𝐵 ) < ( 𝐶 / 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ltdiv2dd.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2 ltdiv2dd.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
3 ltdiv2dd.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
4 ltdiv2dd.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
5 1 2 3 ltdiv2d ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ ( 𝐶 / 𝐵 ) < ( 𝐶 / 𝐴 ) ) )
6 4 5 mpbid ⊢ ( 𝜑 → ( 𝐶 / 𝐵 ) < ( 𝐶 / 𝐴 ) )