# Metamath Proof Explorer

## 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(ℕ\subset ℤ\wedge ℤ\subset ℚ\right)\wedge \left(ℚ\subset ℝ\wedge ℝ\subset ℂ\right)\right)$

### Proof

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