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

Step	Hyp	Ref	Expression
1		0z	$⊢ 0 \in ℤ$
2		divides	$⊢ (0 \in ℤ \land N \in ℤ) \to (0 ∥ N \leftrightarrow \exists n \in ℤ n \cdot 0 = N)$
3	1 2	mpan	$⊢ N \in ℤ \to (0 ∥ N \leftrightarrow \exists n \in ℤ n \cdot 0 = N)$
4		zcn	$⊢ n \in ℤ \to n \in ℂ$
5	4	mul01d	$⊢ n \in ℤ \to n \cdot 0 = 0$
6		eqtr2	$⊢ (n \cdot 0 = N \land n \cdot 0 = 0) \to N = 0$
7	5 6	sylan2	$⊢ (n \cdot 0 = N \land n \in ℤ) \to N = 0$
8	7	ancoms	$⊢ (n \in ℤ \land n \cdot 0 = N) \to N = 0$
9	8	rexlimiva	$⊢ \exists n \in ℤ n \cdot 0 = N \to N = 0$
10	3 9	syl6bi	$⊢ N \in ℤ \to (0 ∥ N \to N = 0)$
11		dvds0	$⊢ 0 \in ℤ \to 0 ∥ 0$
12	1 11	ax-mp	$⊢ 0 ∥ 0$
13		breq2	$⊢ N = 0 \to (0 ∥ N \leftrightarrow 0 ∥ 0)$
14	12 13	mpbiri	$⊢ N = 0 \to 0 ∥ N$
15	10 14	impbid1	$⊢ N \in ℤ \to (0 ∥ N \leftrightarrow N = 0)$

Metamath Proof Explorer