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