Theorem 0dvds

Description: Only 0 is divisible by 0. Theorem 1.1(h) in ApostolNT p. 14. (Contributed by Paul Chapman, 21-Mar-2011)

	Ref	Expression
Assertion	0dvds	|- ( N e. ZZ -> ( 0 || N <-> N = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		0z	|- 0 e. ZZ
2		divides	|- ( ( 0 e. ZZ /\ N e. ZZ ) -> ( 0 || N <-> E. n e. ZZ ( n x. 0 ) = N ) )
3	1 2	mpan	|- ( N e. ZZ -> ( 0 || N <-> E. n e. ZZ ( n x. 0 ) = N ) )
4		zcn	|- ( n e. ZZ -> n e. CC )
5	4	mul01d	|- ( n e. ZZ -> ( n x. 0 ) = 0 )
6		eqtr2	|- ( ( ( n x. 0 ) = N /\ ( n x. 0 ) = 0 ) -> N = 0 )
7	5 6	sylan2	|- ( ( ( n x. 0 ) = N /\ n e. ZZ ) -> N = 0 )
8	7	ancoms	|- ( ( n e. ZZ /\ ( n x. 0 ) = N ) -> N = 0 )
9	8	rexlimiva	|- ( E. n e. ZZ ( n x. 0 ) = N -> N = 0 )
10	3 9	syl6bi	|- ( N e. ZZ -> ( 0 || N -> N = 0 ) )
11		dvds0	|- ( 0 e. ZZ -> 0 || 0 )
12	1 11	ax-mp	|- 0 || 0
13		breq2	|- ( N = 0 -> ( 0 || N <-> 0 || 0 ) )
14	12 13	mpbiri	|- ( N = 0 -> 0 || N )
15	10 14	impbid1	|- ( N e. ZZ -> ( 0 || N <-> N = 0 ) )