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 {\mathbb{Z}}_{\ge 3}$$

Proof

Step	Hyp	Ref	Expression
1		3z	$$⊢3\in \mathbb{Z}$$
2		5nn	$$⊢5\in \mathbb{N}$$
3	2	nnzi	$$⊢5\in \mathbb{Z}$$
4		3re	$$⊢3\in ℝ$$
5		5re	$$⊢5\in ℝ$$
6		3lt5	$$⊢3<5$$
7	4 5 6	ltleii	$$⊢3\le 5$$
8		eluz2	$$⊢5\in {\mathbb{Z}}_{\ge 3}\leftrightarrow \left(3\in \mathbb{Z}\wedge 5\in \mathbb{Z}\wedge 3\le 5\right)$$
9	1 3 7 8	mpbir3an	$$⊢5\in {\mathbb{Z}}_{\ge 3}$$