Metamath Proof Explorer

Theorem 2eluzge1

Description: 2 is an integer greater than or equal to 1. (Contributed by Alexander van der Vekens, 8-Jun-2018)

Ref Expression
Assertion 2eluzge1 ⊢ 2 ∈ ℤ ≥ 1

Proof

Step Hyp Ref Expression
1 1z ⊢ 1 ∈ ℤ
2 2z ⊢ 2 ∈ ℤ
3 1le2 ⊢ 1 ≤ 2
4 eluz2 ⊢ 2 ∈ ℤ ≥ 1 ↔ 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 1 ≤ 2
5 1 2 3 4 mpbir3an ⊢ 2 ∈ ℤ ≥ 1