Metamath Proof Explorer

Theorem ltmulgt11

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

Ref Expression
Assertion ltmulgt11 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 < 𝐵 ↔ 𝐴 < ( 𝐴 · 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 ltmul2 ⊢ ( ( 1 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 1 < 𝐵 ↔ ( 𝐴 · 1 ) < ( 𝐴 · 𝐵 ) ) )
3 1 2 mp3an1 ⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 1 < 𝐵 ↔ ( 𝐴 · 1 ) < ( 𝐴 · 𝐵 ) ) )
4 3 3impb ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 < 𝐵 ↔ ( 𝐴 · 1 ) < ( 𝐴 · 𝐵 ) ) )
5 4 3com12 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 < 𝐵 ↔ ( 𝐴 · 1 ) < ( 𝐴 · 𝐵 ) ) )
6 ax-1rid ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )
7 6 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴 ) → ( 𝐴 · 1 ) = 𝐴 )
8 7 breq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴 ) → ( ( 𝐴 · 1 ) < ( 𝐴 · 𝐵 ) ↔ 𝐴 < ( 𝐴 · 𝐵 ) ) )
9 5 8 bitrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 < 𝐵 ↔ 𝐴 < ( 𝐴 · 𝐵 ) ) )