Theorem nn0p1nn

Description: A nonnegative integer plus 1 is a positive integer. Strengthening of peano2nn . (Contributed by Raph Levien, 30-Jun-2006) (Revised by Mario Carneiro, 16-May-2014)

	Ref	Expression
Assertion	nn0p1nn	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		1nn	⊢ 1 ∈ ℕ
2		nn0nnaddcl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 1 ∈ ℕ ) → ( 𝑁 + 1 ) ∈ ℕ )
3	1 2	mpan2	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )