This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∥ ( 𝑀 · 𝑁 ) )