Metamath Proof Explorer

Theorem lemul1ad

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 lemul1ad φ A C B C


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 lemul1a A B C 0 C A B A C B C
8 1 2 6 5 7 syl31anc φ A C B C