Metamath Proof Explorer

Theorem elnnz

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

Ref Expression
Assertion elnnz ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )

Proof

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