Metamath Proof Explorer

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 syl6bi 
 |-  ( 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 ) )