This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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} \in SubMnd (ℂ_{fld})$

Step	Hyp	Ref	Expression
1		nn0cn	$⊢ x \in ℕ_{0} \to x \in ℂ$
2		nn0addcl	$⊢ (x \in ℕ_{0} \land y \in ℕ_{0}) \to x + y \in ℕ_{0}$
3		0nn0	$⊢ 0 \in ℕ_{0}$
4	1 2 3	cnsubmlem	$⊢ ℕ_{0} \in SubMnd (ℂ_{fld})$