Metamath Proof Explorer

Theorem ltmulgt11

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

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

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 ltmul2 ⊢ 1 ∈ ℝ ∧ B ∈ ℝ ∧ A ∈ ℝ ∧ 0 < A → 1 < B ↔ A ⋅ 1 < A ⁢ B
3 1 2 mp3an1 ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ 0 < A → 1 < B ↔ A ⋅ 1 < A ⁢ B
4 3 3impb ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ 0 < A → 1 < B ↔ A ⋅ 1 < A ⁢ B
5 4 3com12 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < A → 1 < B ↔ A ⋅ 1 < A ⁢ B
6 ax-1rid ⊢ A ∈ ℝ → A ⋅ 1 = A
7 6 3ad2ant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < A → A ⋅ 1 = A
8 7 breq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < A → A ⋅ 1 < A ⁢ B ↔ A < A ⁢ B
9 5 8 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < A → 1 < B ↔ A < A ⁢ B