This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ X \in ℤ_{\geq 4} \to X \in ℕ$

Step	Hyp	Ref	Expression
1		uzuzle24	$⊢ X \in ℤ_{\geq 4} \to X \in ℤ_{\geq 2}$
2		eluz2nn	$⊢ X \in ℤ_{\geq 2} \to X \in ℕ$
3	1 2	syl	$⊢ X \in ℤ_{\geq 4} \to X \in ℕ$