Theorem nthruz

Description: The sequence NN , NN0 , and ZZ forms a chain of proper subsets. In each case the proper subset relationship is shown by demonstrating a number that belongs to one set but not the other. We show that zero belongs to NN0 but not NN and minus one belongs to ZZ but not NN0 . This theorem refines the chain of proper subsets nthruc . (Contributed by NM, 9-May-2004)

	Ref	Expression
Assertion	nthruz	$$⊢\left(\mathbb{N}\subset {\mathbb{N}}_0\wedge {\mathbb{N}}_0\subset \mathbb{Z}\right)$$

Proof

Step	Hyp	Ref	Expression
1		nnssnn0	$$⊢\mathbb{N}\subseteq {\mathbb{N}}_0$$
2		0nn0	$$⊢0\in {\mathbb{N}}_0$$
3		0nnn	$$⊢\neg 0\in \mathbb{N}$$
4	2 3	pm3.2i	$$⊢\left(0\in {\mathbb{N}}_0\wedge \neg 0\in \mathbb{N}\right)$$
5		ssnelpss	$$⊢\mathbb{N}\subseteq {\mathbb{N}}_0\to \left(\left(0\in {\mathbb{N}}_0\wedge \neg 0\in \mathbb{N}\right)\to \mathbb{N}\subset {\mathbb{N}}_0\right)$$
6	1 4 5	mp2	$$⊢\mathbb{N}\subset {\mathbb{N}}_0$$
7		nn0ssz	$$⊢{\mathbb{N}}_0\subseteq \mathbb{Z}$$
8		neg1z	$$⊢-1\in \mathbb{Z}$$
9		neg1lt0	$$⊢-1<0$$
10		nn0nlt0	$$⊢-1\in {\mathbb{N}}_0\to \neg -1<0$$
11	9 10	mt2	$$⊢\neg -1\in {\mathbb{N}}_0$$
12	8 11	pm3.2i	$$⊢\left(-1\in \mathbb{Z}\wedge \neg -1\in {\mathbb{N}}_0\right)$$
13		ssnelpss	$$⊢{\mathbb{N}}_0\subseteq \mathbb{Z}\to \left(\left(-1\in \mathbb{Z}\wedge \neg -1\in {\mathbb{N}}_0\right)\to {\mathbb{N}}_0\subset \mathbb{Z}\right)$$
14	7 12 13	mp2	$$⊢{\mathbb{N}}_0\subset \mathbb{Z}$$
15	6 14	pm3.2i	$$⊢\left(\mathbb{N}\subset {\mathbb{N}}_0\wedge {\mathbb{N}}_0\subset \mathbb{Z}\right)$$