Metamath Proof Explorer


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 )