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

Metamath Proof Explorer

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 ℤ_{\geq 5} \to A \in ℤ_{\geq 3}$

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