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 NNN

Proof

Step Hyp Ref Expression
1 zcn NN
2 1 mulid2d N1 N=N
3 1z 1
4 dvds0lem 1NN1 N=NNN
5 3 4 mp3anl1 NN1 N=NNN
6 5 anabsan N1 N=NNN
7 2 6 mpdan NNN