Theorem elnnnn0c

Description: The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-Jan-2006)

	Ref	Expression
Assertion	elnnnn0c	|- ( N e. NN <-> ( N e. NN0 /\ 1 <_ N ) )

Proof

Step	Hyp	Ref	Expression
1		nnnn0	|- ( N e. NN -> N e. NN0 )
2		nnge1	|- ( N e. NN -> 1 <_ N )
3	1 2	jca	|- ( N e. NN -> ( N e. NN0 /\ 1 <_ N ) )
4		0lt1	|- 0 < 1
5		0re	|- 0 e. RR
6		1re	|- 1 e. RR
7		nn0re	|- ( N e. NN0 -> N e. RR )
8		ltletr	|- ( ( 0 e. RR /\ 1 e. RR /\ N e. RR ) -> ( ( 0 < 1 /\ 1 <_ N ) -> 0 < N ) )
9	5 6 7 8	mp3an12i	|- ( N e. NN0 -> ( ( 0 < 1 /\ 1 <_ N ) -> 0 < N ) )
10	4 9	mpani	|- ( N e. NN0 -> ( 1 <_ N -> 0 < N ) )
11	10	imdistani	|- ( ( N e. NN0 /\ 1 <_ N ) -> ( N e. NN0 /\ 0 < N ) )
12		elnnnn0b	|- ( N e. NN <-> ( N e. NN0 /\ 0 < N ) )
13	11 12	sylibr	|- ( ( N e. NN0 /\ 1 <_ N ) -> N e. NN )
14	3 13	impbii	|- ( N e. NN <-> ( N e. NN0 /\ 1 <_ N ) )