Theorem dvdsmul2

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

	Ref	Expression
Assertion	dvdsmul2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∥ ( 𝑀 · 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		zmulcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
2		eqid	⊢ ( 𝑀 · 𝑁 ) = ( 𝑀 · 𝑁 )
3		dvds0lem	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) ∧ ( 𝑀 · 𝑁 ) = ( 𝑀 · 𝑁 ) ) → 𝑁 ∥ ( 𝑀 · 𝑁 ) )
4	2 3	mpan2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) → 𝑁 ∥ ( 𝑀 · 𝑁 ) )
5	1 4	mpd3an3	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∥ ( 𝑀 · 𝑁 ) )