# 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}\in ℕ↔\left({N}\in ℤ\wedge 0<{N}\right)$

### Proof

Step Hyp Ref Expression
1 nnre ${⊢}{N}\in ℕ\to {N}\in ℝ$
2 orc ${⊢}{N}\in ℕ\to \left({N}\in ℕ\vee \left(-{N}\in ℕ\vee {N}=0\right)\right)$
3 nngt0 ${⊢}{N}\in ℕ\to 0<{N}$
4 1 2 3 jca31 ${⊢}{N}\in ℕ\to \left(\left({N}\in ℝ\wedge \left({N}\in ℕ\vee \left(-{N}\in ℕ\vee {N}=0\right)\right)\right)\wedge 0<{N}\right)$
5 idd ${⊢}\left({N}\in ℝ\wedge 0<{N}\right)\to \left({N}\in ℕ\to {N}\in ℕ\right)$
6 lt0neg2 ${⊢}{N}\in ℝ\to \left(0<{N}↔-{N}<0\right)$
7 renegcl ${⊢}{N}\in ℝ\to -{N}\in ℝ$
8 0re ${⊢}0\in ℝ$
9 ltnsym ${⊢}\left(-{N}\in ℝ\wedge 0\in ℝ\right)\to \left(-{N}<0\to ¬0<-{N}\right)$
10 7 8 9 sylancl ${⊢}{N}\in ℝ\to \left(-{N}<0\to ¬0<-{N}\right)$
11 6 10 sylbid ${⊢}{N}\in ℝ\to \left(0<{N}\to ¬0<-{N}\right)$
12 11 imp ${⊢}\left({N}\in ℝ\wedge 0<{N}\right)\to ¬0<-{N}$
13 nngt0 ${⊢}-{N}\in ℕ\to 0<-{N}$
14 12 13 nsyl ${⊢}\left({N}\in ℝ\wedge 0<{N}\right)\to ¬-{N}\in ℕ$
15 gt0ne0 ${⊢}\left({N}\in ℝ\wedge 0<{N}\right)\to {N}\ne 0$
16 15 neneqd ${⊢}\left({N}\in ℝ\wedge 0<{N}\right)\to ¬{N}=0$
17 ioran ${⊢}¬\left(-{N}\in ℕ\vee {N}=0\right)↔\left(¬-{N}\in ℕ\wedge ¬{N}=0\right)$
18 14 16 17 sylanbrc ${⊢}\left({N}\in ℝ\wedge 0<{N}\right)\to ¬\left(-{N}\in ℕ\vee {N}=0\right)$
19 18 pm2.21d ${⊢}\left({N}\in ℝ\wedge 0<{N}\right)\to \left(\left(-{N}\in ℕ\vee {N}=0\right)\to {N}\in ℕ\right)$
20 5 19 jaod ${⊢}\left({N}\in ℝ\wedge 0<{N}\right)\to \left(\left({N}\in ℕ\vee \left(-{N}\in ℕ\vee {N}=0\right)\right)\to {N}\in ℕ\right)$
21 20 ex ${⊢}{N}\in ℝ\to \left(0<{N}\to \left(\left({N}\in ℕ\vee \left(-{N}\in ℕ\vee {N}=0\right)\right)\to {N}\in ℕ\right)\right)$
22 21 com23 ${⊢}{N}\in ℝ\to \left(\left({N}\in ℕ\vee \left(-{N}\in ℕ\vee {N}=0\right)\right)\to \left(0<{N}\to {N}\in ℕ\right)\right)$
23 22 imp31 ${⊢}\left(\left({N}\in ℝ\wedge \left({N}\in ℕ\vee \left(-{N}\in ℕ\vee {N}=0\right)\right)\right)\wedge 0<{N}\right)\to {N}\in ℕ$
24 4 23 impbii ${⊢}{N}\in ℕ↔\left(\left({N}\in ℝ\wedge \left({N}\in ℕ\vee \left(-{N}\in ℕ\vee {N}=0\right)\right)\right)\wedge 0<{N}\right)$
25 elz ${⊢}{N}\in ℤ↔\left({N}\in ℝ\wedge \left({N}=0\vee {N}\in ℕ\vee -{N}\in ℕ\right)\right)$
26 3orrot ${⊢}\left({N}=0\vee {N}\in ℕ\vee -{N}\in ℕ\right)↔\left({N}\in ℕ\vee -{N}\in ℕ\vee {N}=0\right)$
27 3orass ${⊢}\left({N}\in ℕ\vee -{N}\in ℕ\vee {N}=0\right)↔\left({N}\in ℕ\vee \left(-{N}\in ℕ\vee {N}=0\right)\right)$
28 26 27 bitri ${⊢}\left({N}=0\vee {N}\in ℕ\vee -{N}\in ℕ\right)↔\left({N}\in ℕ\vee \left(-{N}\in ℕ\vee {N}=0\right)\right)$
29 28 anbi2i ${⊢}\left({N}\in ℝ\wedge \left({N}=0\vee {N}\in ℕ\vee -{N}\in ℕ\right)\right)↔\left({N}\in ℝ\wedge \left({N}\in ℕ\vee \left(-{N}\in ℕ\vee {N}=0\right)\right)\right)$
30 25 29 bitri ${⊢}{N}\in ℤ↔\left({N}\in ℝ\wedge \left({N}\in ℕ\vee \left(-{N}\in ℕ\vee {N}=0\right)\right)\right)$
31 30 anbi1i ${⊢}\left({N}\in ℤ\wedge 0<{N}\right)↔\left(\left({N}\in ℝ\wedge \left({N}\in ℕ\vee \left(-{N}\in ℕ\vee {N}=0\right)\right)\right)\wedge 0<{N}\right)$
32 24 31 bitr4i ${⊢}{N}\in ℕ↔\left({N}\in ℤ\wedge 0<{N}\right)$