Theorem znnn0nn

Description: The negative of a negative integer, is a natural number. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	znnn0nn	$$⊢\left(N\in \mathbb{Z}\wedge \neg N\in {\mathbb{N}}_0\right)\to -N\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(N\in \mathbb{Z}\wedge \neg N\in {\mathbb{N}}_0\right)\to N\in \mathbb{Z}$$
2	1	znegcld	$$⊢\left(N\in \mathbb{Z}\wedge \neg N\in {\mathbb{N}}_0\right)\to -N\in \mathbb{Z}$$
3		elznn	$$⊢-N\in \mathbb{Z}\leftrightarrow \left(-N\in ℝ\wedge \left(-N\in \mathbb{N}\vee -\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\in {\mathbb{N}}_0\right)\right)$$
4	2 3	sylib	$$⊢\left(N\in \mathbb{Z}\wedge \neg N\in {\mathbb{N}}_0\right)\to \left(-N\in ℝ\wedge \left(-N\in \mathbb{N}\vee -\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\in {\mathbb{N}}_0\right)\right)$$
5	4	simprd	$$⊢\left(N\in \mathbb{Z}\wedge \neg N\in {\mathbb{N}}_0\right)\to \left(-N\in \mathbb{N}\vee -\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\in {\mathbb{N}}_0\right)$$
6		zcn	$$⊢N\in \mathbb{Z}\to N\in ℂ$$
7	6	adantr	$$⊢\left(N\in \mathbb{Z}\wedge \neg N\in {\mathbb{N}}_0\right)\to N\in ℂ$$
8	7	negnegd	$$⊢\left(N\in \mathbb{Z}\wedge \neg N\in {\mathbb{N}}_0\right)\to -\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}=N$$
9		simpr	$$⊢\left(N\in \mathbb{Z}\wedge \neg N\in {\mathbb{N}}_0\right)\to \neg N\in {\mathbb{N}}_0$$
10	8 9	eqneltrd	$$⊢\left(N\in \mathbb{Z}\wedge \neg N\in {\mathbb{N}}_0\right)\to \neg -\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\in {\mathbb{N}}_0$$
11		pm2.24	$$⊢-\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\in {\mathbb{N}}_0\to \left(\neg -\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\in {\mathbb{N}}_0\to -N\in \mathbb{N}\right)$$
12	11	jao1i	$$⊢\left(-N\in \mathbb{N}\vee -\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\in {\mathbb{N}}_0\right)\to \left(\neg -\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\in {\mathbb{N}}_0\to -N\in \mathbb{N}\right)$$
13	5 10 12	sylc	$$⊢\left(N\in \mathbb{Z}\wedge \neg N\in {\mathbb{N}}_0\right)\to -N\in \mathbb{N}$$