This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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