Theorem nn0sscn

Description: Nonnegative integers are a subset of the complex numbers. (Contributed by NM, 9-May-2004) Reduce dependencies on axioms. (Revised by Steven Nguyen, 8-Oct-2022)

	Ref	Expression
Assertion	nn0sscn	$$⊢{\mathbb{N}}_0\subseteq ℂ$$

Proof

Step	Hyp	Ref	Expression
1		df-n0	$$⊢{\mathbb{N}}_0=\mathbb{N}\cup \left\{0\right\}$$
2		nnsscn	$$⊢\mathbb{N}\subseteq ℂ$$
3		0cn	$$⊢0\in ℂ$$
4		snssi	$$⊢0\in ℂ\to \left\{0\right\}\subseteq ℂ$$
5	3 4	ax-mp	$$⊢\left\{0\right\}\subseteq ℂ$$
6	2 5	unssi	$$⊢\mathbb{N}\cup \left\{0\right\}\subseteq ℂ$$
7	1 6	eqsstri	$$⊢{\mathbb{N}}_0\subseteq ℂ$$