Metamath Proof Explorer


Theorem iddvds

Description: An integer divides itself. Theorem 1.1(a) in ApostolNT p. 14 (reflexive property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion iddvds ( 𝑁 ∈ ℤ → 𝑁𝑁 )

Proof

Step Hyp Ref Expression
1 zcn ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
2 1 mulid2d ( 𝑁 ∈ ℤ → ( 1 · 𝑁 ) = 𝑁 )
3 1z 1 ∈ ℤ
4 dvds0lem ( ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 · 𝑁 ) = 𝑁 ) → 𝑁𝑁 )
5 3 4 mp3anl1 ( ( ( 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 1 · 𝑁 ) = 𝑁 ) → 𝑁𝑁 )
6 5 anabsan ( ( 𝑁 ∈ ℤ ∧ ( 1 · 𝑁 ) = 𝑁 ) → 𝑁𝑁 )
7 2 6 mpdan ( 𝑁 ∈ ℤ → 𝑁𝑁 )