Metamath Proof Explorer

Theorem lemul2a

Description: Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007)

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

Proof

Step Hyp Ref Expression
1 lemul1a 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( A x. C ) <_ ( B x. C ) )
2 recn 
 |-  ( A e. RR -> A e. CC )
3 recn 
 |-  ( C e. RR -> C e. CC )
4 mulcom 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A x. C ) = ( C x. A ) )
5 2 3 4 syl2an 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A x. C ) = ( C x. A ) )
6 5 adantrr 
 |-  ( ( A e. RR /\ ( C e. RR /\ 0 <_ C ) ) -> ( A x. C ) = ( C x. A ) )
7 6 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 <_ C ) ) -> ( A x. C ) = ( C x. A ) )
8 7 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( A x. C ) = ( C x. A ) )
9 recn 
 |-  ( B e. RR -> B e. CC )
10 mulcom 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B x. C ) = ( C x. B ) )
11 9 3 10 syl2an 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B x. C ) = ( C x. B ) )
12 11 adantrr 
 |-  ( ( B e. RR /\ ( C e. RR /\ 0 <_ C ) ) -> ( B x. C ) = ( C x. B ) )
13 12 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 <_ C ) ) -> ( B x. C ) = ( C x. B ) )
14 13 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( B x. C ) = ( C x. B ) )
15 1 8 14 3brtr3d 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( C x. A ) <_ ( C x. B ) )