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