Theorem 2eluzge0

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 )

Proof

Step	Hyp	Ref	Expression
1		2nn0	⊢ 2 ∈ ℕ0
2		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
3	1 2	eleqtri	⊢ 2 ∈ ( ℤ≥ ‘ 0 )