Metamath Proof Explorer

Theorem uz2m1nn

Description: One less than an integer greater than or equal to 2 is a positive integer. (Contributed by Paul Chapman, 17-Nov-2012)

Ref Expression
Assertion uz2m1nn ⊢ N ∈ ℤ ≥ 2 → N − 1 ∈ ℕ

Proof

Step Hyp Ref Expression
1 eluz2b1 ⊢ N ∈ ℤ ≥ 2 ↔ N ∈ ℤ ∧ 1 < N
2 1z ⊢ 1 ∈ ℤ
3 znnsub ⊢ 1 ∈ ℤ ∧ N ∈ ℤ → 1 < N ↔ N − 1 ∈ ℕ
4 2 3 mpan ⊢ N ∈ ℤ → 1 < N ↔ N − 1 ∈ ℕ
5 4 biimpa ⊢ N ∈ ℤ ∧ 1 < N → N − 1 ∈ ℕ
6 1 5 sylbi ⊢ N ∈ ℤ ≥ 2 → N − 1 ∈ ℕ