Theorem dvdsmul2

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

	Ref	Expression
Assertion	dvdsmul2	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to N\parallel \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$

Proof

Step	Hyp	Ref	Expression
1		zmulcl	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{Z}$$
2		eqid	$$⊢\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
3		dvds0lem	$$⊢\left(\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{Z}\right)\wedge \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)\to N\parallel \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
4	2 3	mpan2	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{Z}\right)\to N\parallel \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
5	1 4	mpd3an3	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to N\parallel \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$