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 ) ) )