Database
ELEMENTARY NUMBER THEORY
Elementary properties of divisibility
The divides relation
dvdsmul1
Next ⟩
dvdsmul2
Metamath Proof Explorer
Ascii
Unicode
Theorem
dvdsmul1
Description:
An integer divides a multiple of itself.
(Contributed by
Paul Chapman
, 21-Mar-2011)
Ref
Expression
Assertion
dvdsmul1
⊢
M
∈
ℤ
∧
N
∈
ℤ
→
M
∥
M
⋅
N
Proof
Step
Hyp
Ref
Expression
1
zcn
⊢
N
∈
ℤ
→
N
∈
ℂ
2
zcn
⊢
M
∈
ℤ
→
M
∈
ℂ
3
mulcom
⊢
N
∈
ℂ
∧
M
∈
ℂ
→
N
⋅
M
=
M
⋅
N
4
1
2
3
syl2anr
⊢
M
∈
ℤ
∧
N
∈
ℤ
→
N
⋅
M
=
M
⋅
N
5
zmulcl
⊢
M
∈
ℤ
∧
N
∈
ℤ
→
M
⋅
N
∈
ℤ
6
dvds0lem
⊢
N
∈
ℤ
∧
M
∈
ℤ
∧
M
⋅
N
∈
ℤ
∧
N
⋅
M
=
M
⋅
N
→
M
∥
M
⋅
N
7
6
ex
⊢
N
∈
ℤ
∧
M
∈
ℤ
∧
M
⋅
N
∈
ℤ
→
N
⋅
M
=
M
⋅
N
→
M
∥
M
⋅
N
8
7
3com12
⊢
M
∈
ℤ
∧
N
∈
ℤ
∧
M
⋅
N
∈
ℤ
→
N
⋅
M
=
M
⋅
N
→
M
∥
M
⋅
N
9
5
8
mpd3an3
⊢
M
∈
ℤ
∧
N
∈
ℤ
→
N
⋅
M
=
M
⋅
N
→
M
∥
M
⋅
N
10
4
9
mpd
⊢
M
∈
ℤ
∧
N
∈
ℤ
→
M
∥
M
⋅
N