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	⊢ ( ( ℕ ⊊ ℤ ∧ ℤ ⊊ ℚ ) ∧ ( ℚ ⊊ ℝ ∧ ℝ ⊊ ℂ ) )