Metamath Proof Explorer

Theorem nnnn0addcl

Description: A positive integer plus a nonnegative integer is a positive integer. (Contributed by NM, 20-Apr-2005) (Proof shortened by Mario Carneiro, 16-May-2014)

		Ref	Expression
	Assertion	nnnn0addcl	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to M + N \in ℕ$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
2		nnaddcl	$⊢ (M \in ℕ \land N \in ℕ) \to M + N \in ℕ$
3		oveq2	$⊢ N = 0 \to M + N = M + 0$
4		nncn	$⊢ M \in ℕ \to M \in ℂ$
5	4	addid1d	$⊢ M \in ℕ \to M + 0 = M$
6	3 5	sylan9eqr	$⊢ (M \in ℕ \land N = 0) \to M + N = M$
7		simpl	$⊢ (M \in ℕ \land N = 0) \to M \in ℕ$
8	6 7	eqeltrd	$⊢ (M \in ℕ \land N = 0) \to M + N \in ℕ$
9	2 8	jaodan	$⊢ (M \in ℕ \land (N \in ℕ \lor N = 0)) \to M + N \in ℕ$
10	1 9	sylan2b	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to M + N \in ℕ$