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 ⊢ ℕ ⊂ ℤ ∧ ℤ ⊂ ℚ ∧ ℚ ⊂ ℝ ∧ ℝ ⊂ ℂ

Proof

Step Hyp Ref Expression
1 nnssz ⊢ ℕ ⊆ ℤ
2 0z ⊢ 0 ∈ ℤ
3 0nnn ⊢ ¬ 0 ∈ ℕ
4 2 3 pm3.2i ⊢ 0 ∈ ℤ ∧ ¬ 0 ∈ ℕ
5 ssnelpss ⊢ ℕ ⊆ ℤ → 0 ∈ ℤ ∧ ¬ 0 ∈ ℕ → ℕ ⊂ ℤ
6 1 4 5 mp2 ⊢ ℕ ⊂ ℤ
7 zssq ⊢ ℤ ⊆ ℚ
8 1z ⊢ 1 ∈ ℤ
9 2nn ⊢ 2 ∈ ℕ
10 znq ⊢ 1 ∈ ℤ ∧ 2 ∈ ℕ → 1 2 ∈ ℚ
11 8 9 10 mp2an ⊢ 1 2 ∈ ℚ
12 halfnz ⊢ ¬ 1 2 ∈ ℤ
13 11 12 pm3.2i ⊢ 1 2 ∈ ℚ ∧ ¬ 1 2 ∈ ℤ
14 ssnelpss ⊢ ℤ ⊆ ℚ → 1 2 ∈ ℚ ∧ ¬ 1 2 ∈ ℤ → ℤ ⊂ ℚ
15 7 13 14 mp2 ⊢ ℤ ⊂ ℚ
16 6 15 pm3.2i ⊢ ℕ ⊂ ℤ ∧ ℤ ⊂ ℚ
17 qssre ⊢ ℚ ⊆ ℝ
18 sqrt2re ⊢ 2 ∈ ℝ
19 sqrt2irr ⊢ 2 ∉ ℚ
20 19 neli ⊢ ¬ 2 ∈ ℚ
21 18 20 pm3.2i ⊢ 2 ∈ ℝ ∧ ¬ 2 ∈ ℚ
22 ssnelpss ⊢ ℚ ⊆ ℝ → 2 ∈ ℝ ∧ ¬ 2 ∈ ℚ → ℚ ⊂ ℝ
23 17 21 22 mp2 ⊢ ℚ ⊂ ℝ
24 ax-resscn ⊢ ℝ ⊆ ℂ
25 ax-icn ⊢ i ∈ ℂ
26 inelr ⊢ ¬ i ∈ ℝ
27 25 26 pm3.2i ⊢ i ∈ ℂ ∧ ¬ i ∈ ℝ
28 ssnelpss ⊢ ℝ ⊆ ℂ → i ∈ ℂ ∧ ¬ i ∈ ℝ → ℝ ⊂ ℂ
29 24 27 28 mp2 ⊢ ℝ ⊂ ℂ
30 23 29 pm3.2i ⊢ ℚ ⊂ ℝ ∧ ℝ ⊂ ℂ
31 16 30 pm3.2i ⊢ ℕ ⊂ ℤ ∧ ℤ ⊂ ℚ ∧ ℚ ⊂ ℝ ∧ ℝ ⊂ ℂ