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	⊢ ( ℕ ⊊ ℕ0 ∧ ℕ0 ⊊ ℤ )

Proof

Step	Hyp	Ref	Expression
1		nnssnn0	⊢ ℕ ⊆ ℕ0
2		0nn0	⊢ 0 ∈ ℕ0
3		0nnn	⊢ ¬ 0 ∈ ℕ
4	2 3	pm3.2i	⊢ ( 0 ∈ ℕ0 ∧ ¬ 0 ∈ ℕ )
5		ssnelpss	⊢ ( ℕ ⊆ ℕ0 → ( ( 0 ∈ ℕ0 ∧ ¬ 0 ∈ ℕ ) → ℕ ⊊ ℕ0 ) )
6	1 4 5	mp2	⊢ ℕ ⊊ ℕ0
7		nn0ssz	⊢ ℕ0 ⊆ ℤ
8		neg1z	⊢ - 1 ∈ ℤ
9		neg1lt0	⊢ - 1 < 0
10		nn0nlt0	⊢ ( - 1 ∈ ℕ0 → ¬ - 1 < 0 )
11	9 10	mt2	⊢ ¬ - 1 ∈ ℕ0
12	8 11	pm3.2i	⊢ ( - 1 ∈ ℤ ∧ ¬ - 1 ∈ ℕ0 )
13		ssnelpss	⊢ ( ℕ0 ⊆ ℤ → ( ( - 1 ∈ ℤ ∧ ¬ - 1 ∈ ℕ0 ) → ℕ0 ⊊ ℤ ) )
14	7 12 13	mp2	⊢ ℕ0 ⊊ ℤ
15	6 14	pm3.2i	⊢ ( ℕ ⊊ ℕ0 ∧ ℕ0 ⊊ ℤ )