Metamath Proof Explorer


Theorem dvdsmul1

Description: An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion dvdsmul1 M N M M N

Proof

Step Hyp Ref Expression
1 zcn N N
2 zcn M M
3 mulcom N M N M = M N
4 1 2 3 syl2anr M N N M = M N
5 zmulcl M N M N
6 dvds0lem N M M N N M = M N M M N
7 6 ex N M M N N M = M N M M N
8 7 3com12 M N M N N M = M N M M N
9 5 8 mpd3an3 M N N M = M N M M N
10 4 9 mpd M N M M N