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 ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 0 < 𝑁 ) )

Proof

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