Theorem nn0subm

Description: The nonnegative integers form a submonoid of the complex numbers. (Contributed by Mario Carneiro, 18-Jun-2015)

	Ref	Expression
Assertion	nn0subm	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0cn	$$⊢x\in {\mathbb{N}}_0\to x\in ℂ$$
2		nn0addcl	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\to x+y\in {\mathbb{N}}_0$$
3		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4	1 2 3	cnsubmlem	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$