Metamath Proof Explorer

Theorem lemulge12

Description: Multiplication by a number greater than or equal to 1. (Contributed by Paul Chapman, 21-Mar-2011)

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

Proof

Step Hyp Ref Expression
1 lemulge11 
 |-  ( ( ( 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 breq2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ ( A x. B ) <-> A <_ ( B x. A ) ) )
7 6 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> ( A <_ ( A x. B ) <-> A <_ ( B x. A ) ) )
8 1 7 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> A <_ ( B x. A ) )