Theorem znegcl

Description: Closure law for negative integers. (Contributed by NM, 9-May-2004)

	Ref	Expression
Assertion	znegcl	$$⊢N\in \mathbb{Z}\to -N\in \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		elz	$$⊢N\in \mathbb{Z}\leftrightarrow \left(N\in ℝ\wedge \left(N=0\vee N\in \mathbb{N}\vee -N\in \mathbb{N}\right)\right)$$
2		negeq	$$⊢N=0\to -N=-0$$
3		neg0	$$⊢-0=0$$
4	2 3	eqtrdi	$$⊢N=0\to -N=0$$
5		0z	$$⊢0\in \mathbb{Z}$$
6	4 5	eqeltrdi	$$⊢N=0\to -N\in \mathbb{Z}$$
7		nnnegz	$$⊢N\in \mathbb{N}\to -N\in \mathbb{Z}$$
8		nnz	$$⊢-N\in \mathbb{N}\to -N\in \mathbb{Z}$$
9	6 7 8	3jaoi	$$⊢\left(N=0\vee N\in \mathbb{N}\vee -N\in \mathbb{N}\right)\to -N\in \mathbb{Z}$$
10	1 9	simplbiim	$$⊢N\in \mathbb{Z}\to -N\in \mathbb{Z}$$