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 < 𝑁 ) )