Theorem nn0subm

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

	Ref	Expression
Assertion	nn0subm	⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )

Proof

Step	Hyp	Ref	Expression
1		nn0cn	⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℂ )
2		nn0addcl	⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 + 𝑦 ) ∈ ℕ0 )
3		0nn0	⊢ 0 ∈ ℕ0
4	1 2 3	cnsubmlem	⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )