Metamath Proof Explorer

Theorem lemulge11

Description: Multiplication by a number greater than or equal to 1. (Contributed by NM, 17-Dec-2005)

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

Proof

Step Hyp Ref Expression
1 ax-1rid 
 |-  ( A e. RR -> ( A x. 1 ) = A )
2 1 ad2antrr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> ( A x. 1 ) = A )
3 simpll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> A e. RR )
4 simprl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> 0 <_ A )
5 3 4 jca 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> ( A e. RR /\ 0 <_ A ) )
6 simplr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> B e. RR )
7 1re 
 |-  1 e. RR
8 0le1 
 |-  0 <_ 1
9 7 8 pm3.2i 
 |-  ( 1 e. RR /\ 0 <_ 1 )
10 6 9 jctil 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> ( ( 1 e. RR /\ 0 <_ 1 ) /\ B e. RR ) )
11 5 3 10 jca31 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> ( ( ( A e. RR /\ 0 <_ A ) /\ A e. RR ) /\ ( ( 1 e. RR /\ 0 <_ 1 ) /\ B e. RR ) ) )
12 leid 
 |-  ( A e. RR -> A <_ A )
13 12 ad2antrr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> A <_ A )
14 simprr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> 1 <_ B )
15 13 14 jca 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> ( A <_ A /\ 1 <_ B ) )
16 lemul12a 
 |-  ( ( ( ( A e. RR /\ 0 <_ A ) /\ A e. RR ) /\ ( ( 1 e. RR /\ 0 <_ 1 ) /\ B e. RR ) ) -> ( ( A <_ A /\ 1 <_ B ) -> ( A x. 1 ) <_ ( A x. B ) ) )
17 11 15 16 sylc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> ( A x. 1 ) <_ ( A x. B ) )
18 2 17 eqbrtrrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> A <_ ( A x. B ) )