Metamath Proof Explorer

Theorem elnn0z

Description: Nonnegative integer property expressed in terms of integers. (Contributed by NM, 9-May-2004)

Ref Expression
Assertion elnn0z 
|- ( N e. NN0 <-> ( N e. ZZ /\ 0 <_ N ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 elnnz 
 |-  ( N e. NN <-> ( N e. ZZ /\ 0 < N ) )
3 eqcom 
 |-  ( N = 0 <-> 0 = N )
4 2 3 orbi12i 
 |-  ( ( N e. NN \/ N = 0 ) <-> ( ( N e. ZZ /\ 0 < N ) \/ 0 = N ) )
5 id 
 |-  ( N e. ZZ -> N e. ZZ )
6 0z 
 |-  0 e. ZZ
7 eleq1 
 |-  ( 0 = N -> ( 0 e. ZZ <-> N e. ZZ ) )
8 6 7 mpbii 
 |-  ( 0 = N -> N e. ZZ )
9 5 8 jaoi 
 |-  ( ( N e. ZZ \/ 0 = N ) -> N e. ZZ )
10 orc 
 |-  ( N e. ZZ -> ( N e. ZZ \/ 0 = N ) )
11 9 10 impbii 
 |-  ( ( N e. ZZ \/ 0 = N ) <-> N e. ZZ )
12 11 anbi1i 
 |-  ( ( ( N e. ZZ \/ 0 = N ) /\ ( 0 < N \/ 0 = N ) ) <-> ( N e. ZZ /\ ( 0 < N \/ 0 = N ) ) )
13 ordir 
 |-  ( ( ( N e. ZZ /\ 0 < N ) \/ 0 = N ) <-> ( ( N e. ZZ \/ 0 = N ) /\ ( 0 < N \/ 0 = N ) ) )
14 0re 
 |-  0 e. RR
15 zre 
 |-  ( N e. ZZ -> N e. RR )
16 leloe 
 |-  ( ( 0 e. RR /\ N e. RR ) -> ( 0 <_ N <-> ( 0 < N \/ 0 = N ) ) )
17 14 15 16 sylancr 
 |-  ( N e. ZZ -> ( 0 <_ N <-> ( 0 < N \/ 0 = N ) ) )
18 17 pm5.32i 
 |-  ( ( N e. ZZ /\ 0 <_ N ) <-> ( N e. ZZ /\ ( 0 < N \/ 0 = N ) ) )
19 12 13 18 3bitr4i 
 |-  ( ( ( N e. ZZ /\ 0 < N ) \/ 0 = N ) <-> ( N e. ZZ /\ 0 <_ N ) )
20 1 4 19 3bitri 
 |-  ( N e. NN0 <-> ( N e. ZZ /\ 0 <_ N ) )