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