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	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2		2re	⊢ 2 ∈ ℝ
3		3re	⊢ 3 ∈ ℝ
4		2lt3	⊢ 2 < 3
5	2 3 4	ltleii	⊢ 2 ≤ 3
6		eluzuzle	⊢ ( ( 2 ∈ ℤ ∧ 2 ≤ 3 ) → ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) )
7	1 5 6	mp2an	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )