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	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		nnsscn	⊢ ℕ ⊆ ℂ
2		id	⊢ ( ℕ ⊆ ℂ → ℕ ⊆ ℂ )
3		df-n0	⊢ ℕ0 = ( ℕ ∪ { 0 } )
4		nnaddcl	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 + 𝑁 ) ∈ ℕ )
5	4	adantl	⊢ ( ( ℕ ⊆ ℂ ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) → ( 𝑀 + 𝑁 ) ∈ ℕ )
6	2 3 5	un0addcl	⊢ ( ( ℕ ⊆ ℂ ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ) → ( 𝑀 + 𝑁 ) ∈ ℕ0 )
7	1 6	mpan	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℕ0 )