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

Metamath Proof Explorer

Theorem dvdsmul2

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

Ref Expression
Assertion dvdsmul2 ⊢ M ∈ ℤ ∧ N ∈ ℤ → N ∥ M ⋅ N

Proof

Step Hyp Ref Expression
1 zmulcl ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ⋅ N ∈ ℤ
2 eqid ⊢ M ⋅ N = M ⋅ N
3 dvds0lem ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ⋅ N ∈ ℤ ∧ M ⋅ N = M ⋅ N → N ∥ M ⋅ N
4 2 3 mpan2 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ⋅ N ∈ ℤ → N ∥ M ⋅ N
5 1 4 mpd3an3 ⊢ M ∈ ℤ ∧ N ∈ ℤ → N ∥ M ⋅ N