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

Metamath Proof Explorer

Theorem ltmulgt12d

Description: Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses rpgecld.1 ⊢ φ → A ∈ ℝ
rpgecld.2 ⊢ φ → B ∈ ℝ +
Assertion ltmulgt12d ⊢ φ → 1 < A ↔ B < A ⁢ B

Proof

Step Hyp Ref Expression
1 rpgecld.1 ⊢ φ → A ∈ ℝ
2 rpgecld.2 ⊢ φ → B ∈ ℝ +
3 2 rpred ⊢ φ → B ∈ ℝ
4 2 rpgt0d ⊢ φ → 0 < B
5 ltmulgt12 ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ 0 < B → 1 < A ↔ B < A ⁢ B
6 3 1 4 5 syl3anc ⊢ φ → 1 < A ↔ B < A ⁢ B