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

Metamath Proof Explorer

Theorem elnnnn0b

Description: The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 1-Sep-2005)

Ref Expression
Assertion elnnnn0b ⊢ N ∈ ℕ ↔ N ∈ ℕ 0 ∧ 0 < N

Proof

Step Hyp Ref Expression
1 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
2 nngt0 ⊢ N ∈ ℕ → 0 < N
3 1 2 jca ⊢ N ∈ ℕ → N ∈ ℕ 0 ∧ 0 < N
4 elnn0 ⊢ N ∈ ℕ 0 ↔ N ∈ ℕ ∨ N = 0
5 breq2 ⊢ N = 0 → 0 < N ↔ 0 < 0
6 0re ⊢ 0 ∈ ℝ
7 6 ltnri ⊢ ¬ 0 < 0
8 7 pm2.21i ⊢ 0 < 0 → N ∈ ℕ
9 5 8 biimtrdi ⊢ N = 0 → 0 < N → N ∈ ℕ
10 9 jao1i ⊢ N ∈ ℕ ∨ N = 0 → 0 < N → N ∈ ℕ
11 4 10 sylbi ⊢ N ∈ ℕ 0 → 0 < N → N ∈ ℕ
12 11 imp ⊢ N ∈ ℕ 0 ∧ 0 < N → N ∈ ℕ
13 3 12 impbii ⊢ N ∈ ℕ ↔ N ∈ ℕ 0 ∧ 0 < N