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

Metamath Proof Explorer

Theorem 1eluzge0

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

Ref Expression
Assertion 1eluzge0 ⊢ 1 ∈ ℤ ≥ 0

Proof

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