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

Metamath Proof Explorer

Theorem 5eluz3

Description: 5 is an integer greater than or equal to 3. (Contributed by AV, 7-Sep-2025)

		Ref	Expression
	Assertion	5eluz3	$⊢ 5 \in ℤ_{\geq 3}$

Step	Hyp	Ref	Expression
1		3z	$⊢ 3 \in ℤ$
2		5nn	$⊢ 5 \in ℕ$
3	2	nnzi	$⊢ 5 \in ℤ$
4		3re	$⊢ 3 \in ℝ$
5		5re	$⊢ 5 \in ℝ$
6		3lt5	$⊢ 3 < 5$
7	4 5 6	ltleii	$⊢ 3 \leq 5$
8		eluz2	$⊢ 5 \in ℤ_{\geq 3} \leftrightarrow (3 \in ℤ \land 5 \in ℤ \land 3 \leq 5)$
9	1 3 7 8	mpbir3an	$⊢ 5 \in ℤ_{\geq 3}$