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	|- ( N e. ZZ -> N || N )

Proof

Step	Hyp	Ref	Expression
1		zcn	|- ( N e. ZZ -> N e. CC )
2	1	mulid2d	|- ( N e. ZZ -> ( 1 x. N ) = N )
3		1z	|- 1 e. ZZ
4		dvds0lem	|- ( ( ( 1 e. ZZ /\ N e. ZZ /\ N e. ZZ ) /\ ( 1 x. N ) = N ) -> N || N )
5	3 4	mp3anl1	|- ( ( ( N e. ZZ /\ N e. ZZ ) /\ ( 1 x. N ) = N ) -> N || N )
6	5	anabsan	|- ( ( N e. ZZ /\ ( 1 x. N ) = N ) -> N || N )
7	2 6	mpdan	|- ( N e. ZZ -> N || N )