Metamath Proof Explorer


Theorem lemul1d

Description: Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses ltmul1d.1 φA
ltmul1d.2 φB
ltmul1d.3 φC+
Assertion lemul1d φABACBC

Proof

Step Hyp Ref Expression
1 ltmul1d.1 φA
2 ltmul1d.2 φB
3 ltmul1d.3 φC+
4 3 rpregt0d φC0<C
5 lemul1 ABC0<CABACBC
6 1 2 4 5 syl3anc φABACBC