Theorem peano2zm

Description: "Reverse" second Peano postulate for integers. (Contributed by NM, 12-Sep-2005)

	Ref	Expression
Assertion	peano2zm	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )

Proof

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