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

Proof

Step	Hyp	Ref	Expression
1		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
2	1	mul02d	⊢ ( 𝑁 ∈ ℤ → ( 0 · 𝑁 ) = 0 )
3		0z	⊢ 0 ∈ ℤ
4		dvds0lem	⊢ ( ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 0 ∈ ℤ ) ∧ ( 0 · 𝑁 ) = 0 ) → 𝑁 ∥ 0 )
5	4	ex	⊢ ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 0 ∈ ℤ ) → ( ( 0 · 𝑁 ) = 0 → 𝑁 ∥ 0 ) )
6	3 3 5	mp3an13	⊢ ( 𝑁 ∈ ℤ → ( ( 0 · 𝑁 ) = 0 → 𝑁 ∥ 0 ) )
7	2 6	mpd	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∥ 0 )