Theorem nn0addcl

Description: Closure of addition of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002) (Proof shortened by Mario Carneiro, 17-Jul-2014)

	Ref	Expression
Assertion	nn0addcl	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to M+N\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		nnsscn	$$⊢\mathbb{N}\subseteq ℂ$$
2		id	$$⊢\mathbb{N}\subseteq ℂ\to \mathbb{N}\subseteq ℂ$$
3		df-n0	$$⊢{\mathbb{N}}_0=\mathbb{N}\cup \left\{0\right\}$$
4		nnaddcl	$$⊢\left(M\in \mathbb{N}\wedge N\in \mathbb{N}\right)\to M+N\in \mathbb{N}$$
5	4	adantl	$$⊢\left(\mathbb{N}\subseteq ℂ\wedge \left(M\in \mathbb{N}\wedge N\in \mathbb{N}\right)\right)\to M+N\in \mathbb{N}$$
6	2 3 5	un0addcl	$$⊢\left(\mathbb{N}\subseteq ℂ\wedge \left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\right)\to M+N\in {\mathbb{N}}_0$$
7	1 6	mpan	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to M+N\in {\mathbb{N}}_0$$