Metamath Proof Explorer

Theorem lemul2ad

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

Ref Expression
Hypotheses ltp1d.1 φ A
divgt0d.2 φ B
lemul1ad.3 φ C
lemul1ad.4 φ 0 C
lemul1ad.5 φ A B
Assertion lemul2ad φ C A C B


Step Hyp Ref Expression
1 ltp1d.1 φ A
2 divgt0d.2 φ B
3 lemul1ad.3 φ C
4 lemul1ad.4 φ 0 C
5 lemul1ad.5 φ A B
6 3 4 jca φ C 0 C
7 lemul2a A B C 0 C A B C A C B
8 1 2 6 5 7 syl31anc φ C A C B