Theorem nthruc

Description: The sequence NN , ZZ , QQ , RR , and CC 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 ZZ but not NN , one-half belongs to QQ but not ZZ , the square root of 2 belongs to RR but not QQ , and finally that the imaginary number _i belongs to CC but not RR . See nthruz for a further refinement. (Contributed by NM, 12-Jan-2002)

	Ref	Expression
Assertion	nthruc	$$⊢\left(\left(\mathbb{N}\subset \mathbb{Z}\wedge \mathbb{Z}\subset \mathbb{Q}\right)\wedge \left(\mathbb{Q}\subset ℝ\wedge ℝ\subset ℂ\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		nnssz	$$⊢\mathbb{N}\subseteq \mathbb{Z}$$
2		0z	$$⊢0\in \mathbb{Z}$$
3		0nnn	$$⊢\neg 0\in \mathbb{N}$$
4	2 3	pm3.2i	$$⊢\left(0\in \mathbb{Z}\wedge \neg 0\in \mathbb{N}\right)$$
5		ssnelpss	$$⊢\mathbb{N}\subseteq \mathbb{Z}\to \left(\left(0\in \mathbb{Z}\wedge \neg 0\in \mathbb{N}\right)\to \mathbb{N}\subset \mathbb{Z}\right)$$
6	1 4 5	mp2	$$⊢\mathbb{N}\subset \mathbb{Z}$$
7		zssq	$$⊢\mathbb{Z}\subseteq \mathbb{Q}$$
8		1z	$$⊢1\in \mathbb{Z}$$
9		2nn	$$⊢2\in \mathbb{N}$$
10		znq	$$⊢\left(1\in \mathbb{Z}\wedge 2\in \mathbb{N}\right)\to \frac{1}{2}\in \mathbb{Q}$$
11	8 9 10	mp2an	$$⊢\frac{1}{2}\in \mathbb{Q}$$
12		halfnz	$$⊢\neg \frac{1}{2}\in \mathbb{Z}$$
13	11 12	pm3.2i	$$⊢\left(\frac{1}{2}\in \mathbb{Q}\wedge \neg \frac{1}{2}\in \mathbb{Z}\right)$$
14		ssnelpss	$$⊢\mathbb{Z}\subseteq \mathbb{Q}\to \left(\left(\frac{1}{2}\in \mathbb{Q}\wedge \neg \frac{1}{2}\in \mathbb{Z}\right)\to \mathbb{Z}\subset \mathbb{Q}\right)$$
15	7 13 14	mp2	$$⊢\mathbb{Z}\subset \mathbb{Q}$$
16	6 15	pm3.2i	$$⊢\left(\mathbb{N}\subset \mathbb{Z}\wedge \mathbb{Z}\subset \mathbb{Q}\right)$$
17		qssre	$$⊢\mathbb{Q}\subseteq ℝ$$
18		sqrt2re	$$⊢\sqrt{2}\in ℝ$$
19		sqrt2irr	$$⊢\sqrt{2}\notin \mathbb{Q}$$
20	19	neli	$$⊢\neg \sqrt{2}\in \mathbb{Q}$$
21	18 20	pm3.2i	$$⊢\left(\sqrt{2}\in ℝ\wedge \neg \sqrt{2}\in \mathbb{Q}\right)$$
22		ssnelpss	$$⊢\mathbb{Q}\subseteq ℝ\to \left(\left(\sqrt{2}\in ℝ\wedge \neg \sqrt{2}\in \mathbb{Q}\right)\to \mathbb{Q}\subset ℝ\right)$$
23	17 21 22	mp2	$$⊢\mathbb{Q}\subset ℝ$$
24		ax-resscn	$$⊢ℝ\subseteq ℂ$$
25		ax-icn	$$⊢\mathrm{i}\in ℂ$$
26		inelr	$$⊢\neg \mathrm{i}\in ℝ$$
27	25 26	pm3.2i	$$⊢\left(\mathrm{i}\in ℂ\wedge \neg \mathrm{i}\in ℝ\right)$$
28		ssnelpss	$$⊢ℝ\subseteq ℂ\to \left(\left(\mathrm{i}\in ℂ\wedge \neg \mathrm{i}\in ℝ\right)\to ℝ\subset ℂ\right)$$
29	24 27 28	mp2	$$⊢ℝ\subset ℂ$$
30	23 29	pm3.2i	$$⊢\left(\mathbb{Q}\subset ℝ\wedge ℝ\subset ℂ\right)$$
31	16 30	pm3.2i	$$⊢\left(\left(\mathbb{N}\subset \mathbb{Z}\wedge \mathbb{Z}\subset \mathbb{Q}\right)\wedge \left(\mathbb{Q}\subset ℝ\wedge ℝ\subset ℂ\right)\right)$$