This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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