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

Metamath Proof Explorer

Theorem uzuzle24

Description: An integer greater than or equal to 4 is an integer greater than or equal to 2. (Contributed by AV, 30-May-2023)

		Ref	Expression
	Assertion	uzuzle24	$⊢ X \in ℤ_{\geq 4} \to X \in ℤ_{\geq 2}$

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2		2re	$⊢ 2 \in ℝ$
3		4re	$⊢ 4 \in ℝ$
4		2lt4	$⊢ 2 < 4$
5	2 3 4	ltleii	$⊢ 2 \leq 4$
6		eluzuzle	$⊢ (2 \in ℤ \land 2 \leq 4) \to (X \in ℤ_{\geq 4} \to X \in ℤ_{\geq 2})$
7	1 5 6	mp2an	$⊢ X \in ℤ_{\geq 4} \to X \in ℤ_{\geq 2}$