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	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 1 ) ∈ ℕ )

Proof

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