Theorem nn0zi

Description: A nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014)

	Ref	Expression
Hypothesis	nn0zi.1	⊢ 𝑁 ∈ ℕ0
Assertion	nn0zi	⊢ 𝑁 ∈ ℤ

Proof

Step	Hyp	Ref	Expression
1		nn0zi.1	⊢ 𝑁 ∈ ℕ0
2		nn0ssz	⊢ ℕ0 ⊆ ℤ
3	2 1	sselii	⊢ 𝑁 ∈ ℤ