addclpi

Description: Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995) (New usage is discouraged.)

		Ref	Expression
	Assertion	addclpi	$⊢ (A \in 𝑵 \land B \in 𝑵) \to A +_{𝑵} B \in 𝑵$

Step	Hyp	Ref	Expression
1		addpiord	$⊢ (A \in 𝑵 \land B \in 𝑵) \to A +_{𝑵} B = A +_{𝑜} B$
2		pinn	$⊢ A \in 𝑵 \to A \in ω$
3		pinn	$⊢ B \in 𝑵 \to B \in ω$
4		nnacl	$⊢ (A \in ω \land B \in ω) \to A +_{𝑜} B \in ω$
5	3 4	sylan2	$⊢ (A \in ω \land B \in 𝑵) \to A +_{𝑜} B \in ω$
6		elni2	$⊢ B \in 𝑵 \leftrightarrow (B \in ω \land \emptyset \in B)$
7		nnaordi	$⊢ (B \in ω \land A \in ω) \to (\emptyset \in B \to A +_{𝑜} \emptyset \in (A +_{𝑜} B))$
8		ne0i	$⊢ A +_{𝑜} \emptyset \in (A +_{𝑜} B) \to A +_{𝑜} B \neq \emptyset$
9	7 8	syl6	$⊢ (B \in ω \land A \in ω) \to (\emptyset \in B \to A +_{𝑜} B \neq \emptyset)$
10	9	expcom	$⊢ A \in ω \to (B \in ω \to (\emptyset \in B \to A +_{𝑜} B \neq \emptyset))$
11	10	imp32	$⊢ (A \in ω \land (B \in ω \land \emptyset \in B)) \to A +_{𝑜} B \neq \emptyset$
12	6 11	sylan2b	$⊢ (A \in ω \land B \in 𝑵) \to A +_{𝑜} B \neq \emptyset$
13		elni	$⊢ A +_{𝑜} B \in 𝑵 \leftrightarrow (A +_{𝑜} B \in ω \land A +_{𝑜} B \neq \emptyset)$
14	5 12 13	sylanbrc	$⊢ (A \in ω \land B \in 𝑵) \to A +_{𝑜} B \in 𝑵$
15	2 14	sylan	$⊢ (A \in 𝑵 \land B \in 𝑵) \to A +_{𝑜} B \in 𝑵$
16	1 15	eqeltrd	$⊢ (A \in 𝑵 \land B \in 𝑵) \to A +_{𝑵} B \in 𝑵$

Metamath Proof Explorer