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

Metamath Proof Explorer

Theorem elnnnn0c

Description: The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-Jan-2006)

Ref Expression
Assertion elnnnn0c ⊢ N ∈ ℕ ↔ N ∈ ℕ 0 ∧ 1 ≤ N

Proof

Step Hyp Ref Expression
1 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
2 nnge1 ⊢ N ∈ ℕ → 1 ≤ N
3 1 2 jca ⊢ N ∈ ℕ → N ∈ ℕ 0 ∧ 1 ≤ N
4 0lt1 ⊢ 0 < 1
5 0re ⊢ 0 ∈ ℝ
6 1re ⊢ 1 ∈ ℝ
7 nn0re ⊢ N ∈ ℕ 0 → N ∈ ℝ
8 ltletr ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ N ∈ ℝ → 0 < 1 ∧ 1 ≤ N → 0 < N
9 5 6 7 8 mp3an12i ⊢ N ∈ ℕ 0 → 0 < 1 ∧ 1 ≤ N → 0 < N
10 4 9 mpani ⊢ N ∈ ℕ 0 → 1 ≤ N → 0 < N
11 10 imdistani ⊢ N ∈ ℕ 0 ∧ 1 ≤ N → N ∈ ℕ 0 ∧ 0 < N
12 elnnnn0b ⊢ N ∈ ℕ ↔ N ∈ ℕ 0 ∧ 0 < N
13 11 12 sylibr ⊢ N ∈ ℕ 0 ∧ 1 ≤ N → N ∈ ℕ
14 3 13 impbii ⊢ N ∈ ℕ ↔ N ∈ ℕ 0 ∧ 1 ≤ N