Theorem nnnegz

Description: The negative of a positive integer is an integer. (Contributed by NM, 12-Jan-2002)

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

Proof

Step	Hyp	Ref	Expression
1		nnre	$$⊢N\in \mathbb{N}\to N\in ℝ$$
2	1	renegcld	$$⊢N\in \mathbb{N}\to -N\in ℝ$$
3		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
4		negneg	$$⊢N\in ℂ\to -\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}=N$$
5	4	eleq1d	$$⊢N\in ℂ\to \left(-\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\in \mathbb{N}\leftrightarrow N\in \mathbb{N}\right)$$
6	5	biimprd	$$⊢N\in ℂ\to \left(N\in \mathbb{N}\to -\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\in \mathbb{N}\right)$$
7	3 6	mpcom	$$⊢N\in \mathbb{N}\to -\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\in \mathbb{N}$$
8	7	3mix3d	$$⊢N\in \mathbb{N}\to \left(-N=0\vee -N\in \mathbb{N}\vee -\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\in \mathbb{N}\right)$$
9		elz	$$⊢-N\in \mathbb{Z}\leftrightarrow \left(-N\in ℝ\wedge \left(-N=0\vee -N\in \mathbb{N}\vee -\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\in \mathbb{N}\right)\right)$$
10	2 8 9	sylanbrc	$$⊢N\in \mathbb{N}\to -N\in \mathbb{Z}$$