Metamath Proof Explorer

Theorem peano2z

Description: Second Peano postulate generalized to integers. (Contributed by NM, 13-Feb-2005)

Ref Expression
Assertion peano2z ⊢ N ∈ ℤ → N + 1 ∈ ℤ

Proof

Step Hyp Ref Expression
1 1z ⊢ 1 ∈ ℤ
2 zaddcl ⊢ N ∈ ℤ ∧ 1 ∈ ℤ → N + 1 ∈ ℤ
3 1 2 mpan2 ⊢ N ∈ ℤ → N + 1 ∈ ℤ