# Metamath Proof Explorer

## Theorem elnnz

Description: Positive integer property expressed in terms of integers. (Contributed by NM, 8-Jan-2002)

Ref Expression
Assertion elnnz
`|- ( N e. NN <-> ( N e. ZZ /\ 0 < N ) )`

### Proof

Step Hyp Ref Expression
1 nnre
` |-  ( N e. NN -> N e. RR )`
2 orc
` |-  ( N e. NN -> ( N e. NN \/ ( -u N e. NN \/ N = 0 ) ) )`
3 nngt0
` |-  ( N e. NN -> 0 < N )`
4 1 2 3 jca31
` |-  ( N e. NN -> ( ( N e. RR /\ ( N e. NN \/ ( -u N e. NN \/ N = 0 ) ) ) /\ 0 < N ) )`
5 idd
` |-  ( ( N e. RR /\ 0 < N ) -> ( N e. NN -> N e. NN ) )`
6 lt0neg2
` |-  ( N e. RR -> ( 0 < N <-> -u N < 0 ) )`
7 renegcl
` |-  ( N e. RR -> -u N e. RR )`
8 0re
` |-  0 e. RR`
9 ltnsym
` |-  ( ( -u N e. RR /\ 0 e. RR ) -> ( -u N < 0 -> -. 0 < -u N ) )`
10 7 8 9 sylancl
` |-  ( N e. RR -> ( -u N < 0 -> -. 0 < -u N ) )`
11 6 10 sylbid
` |-  ( N e. RR -> ( 0 < N -> -. 0 < -u N ) )`
12 11 imp
` |-  ( ( N e. RR /\ 0 < N ) -> -. 0 < -u N )`
13 nngt0
` |-  ( -u N e. NN -> 0 < -u N )`
14 12 13 nsyl
` |-  ( ( N e. RR /\ 0 < N ) -> -. -u N e. NN )`
15 gt0ne0
` |-  ( ( N e. RR /\ 0 < N ) -> N =/= 0 )`
16 15 neneqd
` |-  ( ( N e. RR /\ 0 < N ) -> -. N = 0 )`
17 ioran
` |-  ( -. ( -u N e. NN \/ N = 0 ) <-> ( -. -u N e. NN /\ -. N = 0 ) )`
18 14 16 17 sylanbrc
` |-  ( ( N e. RR /\ 0 < N ) -> -. ( -u N e. NN \/ N = 0 ) )`
19 18 pm2.21d
` |-  ( ( N e. RR /\ 0 < N ) -> ( ( -u N e. NN \/ N = 0 ) -> N e. NN ) )`
20 5 19 jaod
` |-  ( ( N e. RR /\ 0 < N ) -> ( ( N e. NN \/ ( -u N e. NN \/ N = 0 ) ) -> N e. NN ) )`
21 20 ex
` |-  ( N e. RR -> ( 0 < N -> ( ( N e. NN \/ ( -u N e. NN \/ N = 0 ) ) -> N e. NN ) ) )`
22 21 com23
` |-  ( N e. RR -> ( ( N e. NN \/ ( -u N e. NN \/ N = 0 ) ) -> ( 0 < N -> N e. NN ) ) )`
23 22 imp31
` |-  ( ( ( N e. RR /\ ( N e. NN \/ ( -u N e. NN \/ N = 0 ) ) ) /\ 0 < N ) -> N e. NN )`
24 4 23 impbii
` |-  ( N e. NN <-> ( ( N e. RR /\ ( N e. NN \/ ( -u N e. NN \/ N = 0 ) ) ) /\ 0 < N ) )`
25 elz
` |-  ( N e. ZZ <-> ( N e. RR /\ ( N = 0 \/ N e. NN \/ -u N e. NN ) ) )`
26 3orrot
` |-  ( ( N = 0 \/ N e. NN \/ -u N e. NN ) <-> ( N e. NN \/ -u N e. NN \/ N = 0 ) )`
27 3orass
` |-  ( ( N e. NN \/ -u N e. NN \/ N = 0 ) <-> ( N e. NN \/ ( -u N e. NN \/ N = 0 ) ) )`
28 26 27 bitri
` |-  ( ( N = 0 \/ N e. NN \/ -u N e. NN ) <-> ( N e. NN \/ ( -u N e. NN \/ N = 0 ) ) )`
29 28 anbi2i
` |-  ( ( N e. RR /\ ( N = 0 \/ N e. NN \/ -u N e. NN ) ) <-> ( N e. RR /\ ( N e. NN \/ ( -u N e. NN \/ N = 0 ) ) ) )`
30 25 29 bitri
` |-  ( N e. ZZ <-> ( N e. RR /\ ( N e. NN \/ ( -u N e. NN \/ N = 0 ) ) ) )`
31 30 anbi1i
` |-  ( ( N e. ZZ /\ 0 < N ) <-> ( ( N e. RR /\ ( N e. NN \/ ( -u N e. NN \/ N = 0 ) ) ) /\ 0 < N ) )`
32 24 31 bitr4i
` |-  ( N e. NN <-> ( N e. ZZ /\ 0 < N ) )`