Theorem nn0nnaddcl

Description: A nonnegative integer plus a positive integer is a positive integer. (Contributed by NM, 22-Dec-2005)

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

Proof

Step	Hyp	Ref	Expression
1		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
2		nn0cn	$$⊢M\in {\mathbb{N}}_0\to M\in ℂ$$
3		addcom	$$⊢\left(N\in ℂ\wedge M\in ℂ\right)\to N+M=M+N$$
4	1 2 3	syl2an	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to N+M=M+N$$
5		nnnn0addcl	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to N+M\in \mathbb{N}$$
6	4 5	eqeltrrd	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to M+N\in \mathbb{N}$$
7	6	ancoms	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in \mathbb{N}\right)\to M+N\in \mathbb{N}$$