This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elnnz1

Description: Positive integer property expressed in terms of integers. (Contributed by NM, 10-May-2004) (Proof shortened by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion elnnz1 ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 1 ≤ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
2 nnge1 ⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 )
3 1 2 jca ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℤ ∧ 1 ≤ 𝑁 ) )
4 0lt1 ⊢ 0 < 1
5 0re ⊢ 0 ∈ ℝ
6 1re ⊢ 1 ∈ ℝ
7 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
8 ltletr ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 0 < 1 ∧ 1 ≤ 𝑁 ) → 0 < 𝑁 ) )
9 5 6 7 8 mp3an12i ⊢ ( 𝑁 ∈ ℤ → ( ( 0 < 1 ∧ 1 ≤ 𝑁 ) → 0 < 𝑁 ) )
10 4 9 mpani ⊢ ( 𝑁 ∈ ℤ → ( 1 ≤ 𝑁 → 0 < 𝑁 ) )
11 10 imdistani ⊢ ( ( 𝑁 ∈ ℤ ∧ 1 ≤ 𝑁 ) → ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
12 elnnz ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
13 11 12 sylibr ⊢ ( ( 𝑁 ∈ ℤ ∧ 1 ≤ 𝑁 ) → 𝑁 ∈ ℕ )
14 3 13 impbii ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 1 ≤ 𝑁 ) )