Theorem eluz4nn

Description: An integer greater than or equal to 4 is a positive integer. (Contributed by AV, 30-May-2023)

	Ref	Expression
Assertion	eluz4nn	⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → 𝑋 ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		eluz4eluz2	⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → 𝑋 ∈ ( ℤ≥ ‘ 2 ) )
2		eluz2nn	⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) → 𝑋 ∈ ℕ )
3	1 2	syl	⊢ ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → 𝑋 ∈ ℕ )