Theorem elnnnn0b

Description: The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 1-Sep-2005)

	Ref	Expression
Assertion	elnnnn0b	|- ( N e. NN <-> ( N e. NN0 /\ 0 < N ) )

Proof

Step	Hyp	Ref	Expression
1		nnnn0	|- ( N e. NN -> N e. NN0 )
2		nngt0	|- ( N e. NN -> 0 < N )
3	1 2	jca	|- ( N e. NN -> ( N e. NN0 /\ 0 < N ) )
4		elnn0	|- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
5		breq2	|- ( N = 0 -> ( 0 < N <-> 0 < 0 ) )
6		0re	|- 0 e. RR
7	6	ltnri	|- -. 0 < 0
8	7	pm2.21i	|- ( 0 < 0 -> N e. NN )
9	5 8	biimtrdi	|- ( N = 0 -> ( 0 < N -> N e. NN ) )
10	9	jao1i	|- ( ( N e. NN \/ N = 0 ) -> ( 0 < N -> N e. NN ) )
11	4 10	sylbi	|- ( N e. NN0 -> ( 0 < N -> N e. NN ) )
12	11	imp	|- ( ( N e. NN0 /\ 0 < N ) -> N e. NN )
13	3 12	impbii	|- ( N e. NN <-> ( N e. NN0 /\ 0 < N ) )