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 N 0 < N

Proof

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