Metamath Proof Explorer

Theorem 1dvds

Description: 1 divides any integer. Theorem 1.1(f) in ApostolNT p. 14. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion 1dvds 
|- ( N e. ZZ -> 1 || N )

Proof

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