# Metamath Proof Explorer

## Theorem dvdsmul1

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

Ref Expression
Assertion dvdsmul1 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}\parallel {M}\cdot {N}$

### Proof

Step Hyp Ref Expression
1 zcn ${⊢}{N}\in ℤ\to {N}\in ℂ$
2 zcn ${⊢}{M}\in ℤ\to {M}\in ℂ$
3 mulcom ${⊢}\left({N}\in ℂ\wedge {M}\in ℂ\right)\to {N}\cdot {M}={M}\cdot {N}$
4 1 2 3 syl2anr ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {N}\cdot {M}={M}\cdot {N}$
5 zmulcl ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}\cdot {N}\in ℤ$
6 dvds0lem ${⊢}\left(\left({N}\in ℤ\wedge {M}\in ℤ\wedge {M}\cdot {N}\in ℤ\right)\wedge {N}\cdot {M}={M}\cdot {N}\right)\to {M}\parallel {M}\cdot {N}$
7 6 ex ${⊢}\left({N}\in ℤ\wedge {M}\in ℤ\wedge {M}\cdot {N}\in ℤ\right)\to \left({N}\cdot {M}={M}\cdot {N}\to {M}\parallel {M}\cdot {N}\right)$
8 7 3com12 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {M}\cdot {N}\in ℤ\right)\to \left({N}\cdot {M}={M}\cdot {N}\to {M}\parallel {M}\cdot {N}\right)$
9 5 8 mpd3an3 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({N}\cdot {M}={M}\cdot {N}\to {M}\parallel {M}\cdot {N}\right)$
10 4 9 mpd ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}\parallel {M}\cdot {N}$