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