Theorem uzuzle35

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

	Ref	Expression
Assertion	uzuzle35	$$⊢A\in {\mathbb{Z}}_{\ge 5}\to A\in {\mathbb{Z}}_{\ge 3}$$

Proof

Step	Hyp	Ref	Expression
1		5eluz3	$$⊢5\in {\mathbb{Z}}_{\ge 3}$$
2		uzss	$$⊢5\in {\mathbb{Z}}_{\ge 3}\to {\mathbb{Z}}_{\ge 5}\subseteq {\mathbb{Z}}_{\ge 3}$$
3	1 2	ax-mp	$$⊢{\mathbb{Z}}_{\ge 5}\subseteq {\mathbb{Z}}_{\ge 3}$$
4	3	sseli	$$⊢A\in {\mathbb{Z}}_{\ge 5}\to A\in {\mathbb{Z}}_{\ge 3}$$