Metamath Proof Explorer

Theorem peano2zm

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

Ref Expression
Assertion peano2zm ⊢ N ∈ ℤ → N − 1 ∈ ℤ

Proof

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