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

Metamath Proof Explorer

Theorem uzuzle23

Description: An integer greater than or equal to 3 is an integer greater than or equal to 2. (Contributed by Alexander van der Vekens, 17-Sep-2018)

		Ref	Expression
	Assertion	uzuzle23	$⊢ A \in ℤ_{\geq 3} \to A \in ℤ_{\geq 2}$

Proof

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