This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in ℤ \to N ∥ 0$

Step	Hyp	Ref	Expression
1		zcn	$⊢ N \in ℤ \to N \in ℂ$
2	1	mul02d	$⊢ N \in ℤ \to 0 \cdot N = 0$
3		0z	$⊢ 0 \in ℤ$
4		dvds0lem	$⊢ ((0 \in ℤ \land N \in ℤ \land 0 \in ℤ) \land 0 \cdot N = 0) \to N ∥ 0$
5	4	ex	$⊢ (0 \in ℤ \land N \in ℤ \land 0 \in ℤ) \to (0 \cdot N = 0 \to N ∥ 0)$
6	3 3 5	mp3an13	$⊢ N \in ℤ \to (0 \cdot N = 0 \to N ∥ 0)$
7	2 6	mpd	$⊢ N \in ℤ \to N ∥ 0$