Theorem uzuzle23

Description: An integer in the upper set of integers starting at 3 is element of the upper set of integers starting at 2. (Contributed by Alexander van der Vekens, 17-Sep-2018)

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

Proof

Step	Hyp	Ref	Expression
1		2z	$$⊢2\in \mathbb{Z}$$
2		2re	$$⊢2\in ℝ$$
3		3re	$$⊢3\in ℝ$$
4		2lt3	$$⊢2<3$$
5	2 3 4	ltleii	$$⊢2\le 3$$
6		eluzuzle	$$⊢\left(2\in \mathbb{Z}\wedge 2\le 3\right)\to \left(A\in {\mathbb{Z}}_{\ge 3}\to A\in {\mathbb{Z}}_{\ge 2}\right)$$
7	1 5 6	mp2an	$$⊢A\in {\mathbb{Z}}_{\ge 3}\to A\in {\mathbb{Z}}_{\ge 2}$$