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	|- ( NN C. NN0 /\ NN0 C. ZZ )

Proof

Step	Hyp	Ref	Expression
1		nnssnn0	|- NN C_ NN0
2		0nn0	|- 0 e. NN0
3		0nnn	|- -. 0 e. NN
4	2 3	pm3.2i	|- ( 0 e. NN0 /\ -. 0 e. NN )
5		ssnelpss	|- ( NN C_ NN0 -> ( ( 0 e. NN0 /\ -. 0 e. NN ) -> NN C. NN0 ) )
6	1 4 5	mp2	|- NN C. NN0
7		nn0ssz	|- NN0 C_ ZZ
8		neg1z	|- -u 1 e. ZZ
9		neg1lt0	|- -u 1 < 0
10		nn0nlt0	|- ( -u 1 e. NN0 -> -. -u 1 < 0 )
11	9 10	mt2	|- -. -u 1 e. NN0
12	8 11	pm3.2i	|- ( -u 1 e. ZZ /\ -. -u 1 e. NN0 )
13		ssnelpss	|- ( NN0 C_ ZZ -> ( ( -u 1 e. ZZ /\ -. -u 1 e. NN0 ) -> NN0 C. ZZ ) )
14	7 12 13	mp2	|- NN0 C. ZZ
15	6 14	pm3.2i	|- ( NN C. NN0 /\ NN0 C. ZZ )