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 ( 𝐴 ∈ ( ℤ≥ ‘ 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 ) )