Description: 2 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018) (Proof shortened by OpenAI, 25-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | 2eluzge0 | ⊢ 2 ∈ ( ℤ_{≥} ‘ 0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2nn0 | ⊢ 2 ∈ ℕ_{0} | |
2 | nn0uz | ⊢ ℕ_{0} = ( ℤ_{≥} ‘ 0 ) | |
3 | 1 2 | eleqtri | ⊢ 2 ∈ ( ℤ_{≥} ‘ 0 ) |