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

Metamath Proof Explorer

Theorem uzuzle24

Description: An integer greater than or equal to 4 is an integer greater than or equal to 2. (Contributed by AV, 30-May-2023)

Ref Expression
Assertion uzuzle24 ( 𝑋 ∈ ( ℤ≥ ‘ 4 ) → 𝑋 ∈ ( ℤ≥ ‘ 2 ) )

Proof

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