Theorem elnnnn0c

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

	Ref	Expression
Assertion	elnnnn0c	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁 ) )

Proof

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