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	⊢ ( 𝑁 ∈ ℤ → ( 0 ∥ 𝑁 ↔ 𝑁 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		0z	⊢ 0 ∈ ℤ
2		divides	⊢ ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 0 ) = 𝑁 ) )
3	1 2	mpan	⊢ ( 𝑁 ∈ ℤ → ( 0 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 · 0 ) = 𝑁 ) )
4		zcn	⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
5	4	mul01d	⊢ ( 𝑛 ∈ ℤ → ( 𝑛 · 0 ) = 0 )
6		eqtr2	⊢ ( ( ( 𝑛 · 0 ) = 𝑁 ∧ ( 𝑛 · 0 ) = 0 ) → 𝑁 = 0 )
7	5 6	sylan2	⊢ ( ( ( 𝑛 · 0 ) = 𝑁 ∧ 𝑛 ∈ ℤ ) → 𝑁 = 0 )
8	7	ancoms	⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑛 · 0 ) = 𝑁 ) → 𝑁 = 0 )
9	8	rexlimiva	⊢ ( ∃ 𝑛 ∈ ℤ ( 𝑛 · 0 ) = 𝑁 → 𝑁 = 0 )
10	3 9	biimtrdi	⊢ ( 𝑁 ∈ ℤ → ( 0 ∥ 𝑁 → 𝑁 = 0 ) )
11		dvds0	⊢ ( 0 ∈ ℤ → 0 ∥ 0 )
12	1 11	ax-mp	⊢ 0 ∥ 0
13		breq2	⊢ ( 𝑁 = 0 → ( 0 ∥ 𝑁 ↔ 0 ∥ 0 ) )
14	12 13	mpbiri	⊢ ( 𝑁 = 0 → 0 ∥ 𝑁 )
15	10 14	impbid1	⊢ ( 𝑁 ∈ ℤ → ( 0 ∥ 𝑁 ↔ 𝑁 = 0 ) )