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

Metamath Proof Explorer

Theorem eluz2nn

Description: An integer greater than or equal to 2 is a positive integer. (Contributed by AV, 3-Nov-2018)

		Ref	Expression
	Assertion	eluz2nn	$⊢ A \in ℤ_{\geq 2} \to A \in ℕ$

Step	Hyp	Ref	Expression
1		1z	$⊢ 1 \in ℤ$
2		1le2	$⊢ 1 \leq 2$
3		eluzuzle	$⊢ (1 \in ℤ \land 1 \leq 2) \to (A \in ℤ_{\geq 2} \to A \in ℤ_{\geq 1})$
4	1 2 3	mp2an	$⊢ A \in ℤ_{\geq 2} \to A \in ℤ_{\geq 1}$
5		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
6	4 5	eleqtrrdi	$⊢ A \in ℤ_{\geq 2} \to A \in ℕ$