Theorem peano2z

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

	Ref	Expression
Assertion	peano2z	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + 1 ) ∈ ℤ )

Proof

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