Theorem dvdsmul1

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

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

Proof

Step	Hyp	Ref	Expression
1		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
2		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
3		mulcom	⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝑁 · 𝑀 ) = ( 𝑀 · 𝑁 ) )
4	1 2 3	syl2anr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 · 𝑀 ) = ( 𝑀 · 𝑁 ) )
5		zmulcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
6		dvds0lem	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) ∧ ( 𝑁 · 𝑀 ) = ( 𝑀 · 𝑁 ) ) → 𝑀 ∥ ( 𝑀 · 𝑁 ) )
7	6	ex	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) → ( ( 𝑁 · 𝑀 ) = ( 𝑀 · 𝑁 ) → 𝑀 ∥ ( 𝑀 · 𝑁 ) ) )
8	7	3com12	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) → ( ( 𝑁 · 𝑀 ) = ( 𝑀 · 𝑁 ) → 𝑀 ∥ ( 𝑀 · 𝑁 ) ) )
9	5 8	mpd3an3	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 · 𝑀 ) = ( 𝑀 · 𝑁 ) → 𝑀 ∥ ( 𝑀 · 𝑁 ) ) )
10	4 9	mpd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∥ ( 𝑀 · 𝑁 ) )