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

Metamath Proof Explorer

Theorem uzuzle34

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

		Ref	Expression
	Assertion	uzuzle34	$⊢ X \in ℤ_{\geq 4} \to X \in ℤ_{\geq 3}$

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