Theorem peano2nn0

Description: Second Peano postulate for nonnegative integers. (Contributed by NM, 9-May-2004)

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

Proof

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