Metamath Proof Explorer


Theorem ltmulgt12

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

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

Proof

Step Hyp Ref Expression
1 ltmulgt11
 |-  ( ( A e. RR /\ B e. RR /\ 0 < A ) -> ( 1 < B <-> A < ( A x. B ) ) )
2 recn
 |-  ( A e. RR -> A e. CC )
3 recn
 |-  ( B e. RR -> B e. CC )
4 mulcom
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
5 2 3 4 syl2an
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) = ( B x. A ) )
6 5 3adant3
 |-  ( ( A e. RR /\ B e. RR /\ 0 < A ) -> ( A x. B ) = ( B x. A ) )
7 6 breq2d
 |-  ( ( A e. RR /\ B e. RR /\ 0 < A ) -> ( A < ( A x. B ) <-> A < ( B x. A ) ) )
8 1 7 bitrd
 |-  ( ( A e. RR /\ B e. RR /\ 0 < A ) -> ( 1 < B <-> A < ( B x. A ) ) )