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