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∈ℤ