# 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 ) )`