Metamath Proof Explorer


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 ) )