Metamath Proof Explorer


Theorem ltmulgt11

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

Ref Expression
Assertion ltmulgt11
|- ( ( A e. RR /\ B e. RR /\ 0 < A ) -> ( 1 < B <-> A < ( A x. B ) ) )

Proof

Step Hyp Ref Expression
1 1re
 |-  1 e. RR
2 ltmul2
 |-  ( ( 1 e. RR /\ B e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( 1 < B <-> ( A x. 1 ) < ( A x. B ) ) )
3 1 2 mp3an1
 |-  ( ( B e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( 1 < B <-> ( A x. 1 ) < ( A x. B ) ) )
4 3 3impb
 |-  ( ( B e. RR /\ A e. RR /\ 0 < A ) -> ( 1 < B <-> ( A x. 1 ) < ( A x. B ) ) )
5 4 3com12
 |-  ( ( A e. RR /\ B e. RR /\ 0 < A ) -> ( 1 < B <-> ( A x. 1 ) < ( A x. B ) ) )
6 ax-1rid
 |-  ( A e. RR -> ( A x. 1 ) = A )
7 6 3ad2ant1
 |-  ( ( A e. RR /\ B e. RR /\ 0 < A ) -> ( A x. 1 ) = A )
8 7 breq1d
 |-  ( ( A e. RR /\ B e. RR /\ 0 < A ) -> ( ( A x. 1 ) < ( A x. B ) <-> A < ( A x. B ) ) )
9 5 8 bitrd
 |-  ( ( A e. RR /\ B e. RR /\ 0 < A ) -> ( 1 < B <-> A < ( A x. B ) ) )