Theorem nn0ge2m1nnALT

Description: Alternate proof of nn0ge2m1nn : If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is a positive integer. This version is proved using eluz2 , a theorem for upper sets of integers, which are defined later than the positive and nonnegative integers. This proof is, however, much shorter than the proof of nn0ge2m1nn . (Contributed by Alexander van der Vekens, 1-Aug-2018) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	nn0ge2m1nnALT	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2	1	a1i	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → 2 ∈ ℤ )
3		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
4	3	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → 𝑁 ∈ ℤ )
5		simpr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → 2 ≤ 𝑁 )
6		eluz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) )
7	2 4 5 6	syl3anbrc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
8		uz2m1nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 − 1 ) ∈ ℕ )
9	7 8	syl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ℕ )