Theorem dvdsmul2

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

	Ref	Expression
Assertion	dvdsmul2	|- ( ( M e. ZZ /\ N e. ZZ ) -> N || ( M x. N ) )

Proof

Step	Hyp	Ref	Expression
1		zmulcl	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )
2		eqid	|- ( M x. N ) = ( M x. N )
3		dvds0lem	|- ( ( ( M e. ZZ /\ N e. ZZ /\ ( M x. N ) e. ZZ ) /\ ( M x. N ) = ( M x. N ) ) -> N || ( M x. N ) )
4	2 3	mpan2	|- ( ( M e. ZZ /\ N e. ZZ /\ ( M x. N ) e. ZZ ) -> N || ( M x. N ) )
5	1 4	mpd3an3	|- ( ( M e. ZZ /\ N e. ZZ ) -> N || ( M x. N ) )