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 )