Theorem 5eluz3

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

	Ref	Expression
Assertion	5eluz3	⊢ 5 ∈ ( ℤ≥ ‘ 3 )

Proof

Step	Hyp	Ref	Expression
1		3z	⊢ 3 ∈ ℤ
2		5nn	⊢ 5 ∈ ℕ
3	2	nnzi	⊢ 5 ∈ ℤ
4		3re	⊢ 3 ∈ ℝ
5		5re	⊢ 5 ∈ ℝ
6		3lt5	⊢ 3 < 5
7	4 5 6	ltleii	⊢ 3 ≤ 5
8		eluz2	⊢ ( 5 ∈ ( ℤ≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ 5 ∈ ℤ ∧ 3 ≤ 5 ) )
9	1 3 7 8	mpbir3an	⊢ 5 ∈ ( ℤ≥ ‘ 3 )