Metamath Proof Explorer


Theorem dvdsmultr2

Description: If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012)

Ref Expression
Assertion dvdsmultr2 KMNKNK M N

Proof

Step Hyp Ref Expression
1 dvdsmul2 MNN M N
2 1 biantrud MNKNKNN M N
3 2 3adant1 KMNKNKNN M N
4 simp1 KMNK
5 simp3 KMNN
6 zmulcl MN M N
7 6 3adant1 KMN M N
8 dvdstr KN M NKNN M NK M N
9 4 5 7 8 syl3anc KMNKNN M NK M N
10 3 9 sylbid KMNKNK M N