Metamath Proof Explorer

Theorem addclpi

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

Ref Expression
Assertion addclpi ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A + 𝑵 B ∈ 𝑵

Proof

Step Hyp Ref Expression
1 addpiord ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A + 𝑵 B = A + 𝑜 B
2 pinn ⊢ A ∈ 𝑵 → A ∈ ω
3 pinn ⊢ B ∈ 𝑵 → B ∈ ω
4 nnacl ⊢ A ∈ ω ∧ B ∈ ω → A + 𝑜 B ∈ ω
5 3 4 sylan2 ⊢ A ∈ ω ∧ B ∈ 𝑵 → A + 𝑜 B ∈ ω
6 elni2 ⊢ B ∈ 𝑵 ↔ B ∈ ω ∧ ∅ ∈ B
7 nnaordi ⊢ B ∈ ω ∧ A ∈ ω → ∅ ∈ B → A + 𝑜 ∅ ∈ A + 𝑜 B
8 ne0i ⊢ A + 𝑜 ∅ ∈ A + 𝑜 B → A + 𝑜 B ≠ ∅
9 7 8 syl6 ⊢ B ∈ ω ∧ A ∈ ω → ∅ ∈ B → A + 𝑜 B ≠ ∅
10 9 expcom ⊢ A ∈ ω → B ∈ ω → ∅ ∈ B → A + 𝑜 B ≠ ∅
11 10 imp32 ⊢ A ∈ ω ∧ B ∈ ω ∧ ∅ ∈ B → A + 𝑜 B ≠ ∅
12 6 11 sylan2b ⊢ A ∈ ω ∧ B ∈ 𝑵 → A + 𝑜 B ≠ ∅
13 elni ⊢ A + 𝑜 B ∈ 𝑵 ↔ A + 𝑜 B ∈ ω ∧ A + 𝑜 B ≠ ∅
14 5 12 13 sylanbrc ⊢ A ∈ ω ∧ B ∈ 𝑵 → A + 𝑜 B ∈ 𝑵
15 2 14 sylan ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A + 𝑜 B ∈ 𝑵
16 1 15 eqeltrd ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A + 𝑵 B ∈ 𝑵