Metamath Proof Explorer

Theorem ltmulgt12

Description: Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005)

Ref Expression
Assertion ltmulgt12 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < A → 1 < B ↔ A < B ⁢ A

Proof

Step Hyp Ref Expression
1 ltmulgt11 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < A → 1 < B ↔ A < A ⁢ B
2 recn ⊢ A ∈ ℝ → A ∈ ℂ
3 recn ⊢ B ∈ ℝ → B ∈ ℂ
4 mulcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = B ⁢ A
5 2 3 4 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ⁢ B = B ⁢ A
6 5 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < A → A ⁢ B = B ⁢ A
7 6 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < A → A < A ⁢ B ↔ A < B ⁢ A
8 1 7 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < A → 1 < B ↔ A < B ⁢ A