Metamath Proof Explorer


Theorem elnnz

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

Ref Expression
Assertion elnnz NN0<N

Proof

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