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 ABC0CABCACB

Proof

Step Hyp Ref Expression
1 lemul1a ABC0CABACBC
2 recn AA
3 recn CC
4 mulcom ACAC=CA
5 2 3 4 syl2an ACAC=CA
6 5 adantrr AC0CAC=CA
7 6 3adant2 ABC0CAC=CA
8 7 adantr ABC0CABAC=CA
9 recn BB
10 mulcom BCBC=CB
11 9 3 10 syl2an BCBC=CB
12 11 adantrr BC0CBC=CB
13 12 3adant1 ABC0CBC=CB
14 13 adantr ABC0CABBC=CB
15 1 8 14 3brtr3d ABC0CABCACB