Metamath Proof Explorer

Theorem dvds0

Description: Any integer divides 0. Theorem 1.1(g) in ApostolNT p. 14. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion dvds0 
|- ( N e. ZZ -> N || 0 )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( N e. ZZ -> N e. CC )
2 1 mul02d 
 |-  ( N e. ZZ -> ( 0 x. N ) = 0 )
3 0z 
 |-  0 e. ZZ
4 dvds0lem 
 |-  ( ( ( 0 e. ZZ /\ N e. ZZ /\ 0 e. ZZ ) /\ ( 0 x. N ) = 0 ) -> N || 0 )
5 4 ex 
 |-  ( ( 0 e. ZZ /\ N e. ZZ /\ 0 e. ZZ ) -> ( ( 0 x. N ) = 0 -> N || 0 ) )
6 3 3 5 mp3an13 
 |-  ( N e. ZZ -> ( ( 0 x. N ) = 0 -> N || 0 ) )
7 2 6 mpd 
 |-  ( N e. ZZ -> N || 0 )