Theorem nn0nnaddcl

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

	Ref	Expression
Assertion	nn0nnaddcl	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝑀 + 𝑁 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
2		nn0cn	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ )
3		addcom	⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝑁 + 𝑀 ) = ( 𝑀 + 𝑁 ) )
4	1 2 3	syl2an	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 + 𝑀 ) = ( 𝑀 + 𝑁 ) )
5		nnnn0addcl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 + 𝑀 ) ∈ ℕ )
6	4 5	eqeltrrd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℕ )
7	6	ancoms	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝑀 + 𝑁 ) ∈ ℕ )