Metamath Proof Explorer

Theorem nnaddcl

Description: Closure of addition of positive integers, proved by induction on the second addend. (Contributed by NM, 12-Jan-1997)

Ref Expression
Assertion nnaddcl ⊢ A ∈ ℕ ∧ B ∈ ℕ → A + B ∈ ℕ

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ x = 1 → A + x = A + 1
2 1 eleq1d ⊢ x = 1 → A + x ∈ ℕ ↔ A + 1 ∈ ℕ
3 2 imbi2d ⊢ x = 1 → A ∈ ℕ → A + x ∈ ℕ ↔ A ∈ ℕ → A + 1 ∈ ℕ
4 oveq2 ⊢ x = y → A + x = A + y
5 4 eleq1d ⊢ x = y → A + x ∈ ℕ ↔ A + y ∈ ℕ
6 5 imbi2d ⊢ x = y → A ∈ ℕ → A + x ∈ ℕ ↔ A ∈ ℕ → A + y ∈ ℕ
7 oveq2 ⊢ x = y + 1 → A + x = A + y + 1
8 7 eleq1d ⊢ x = y + 1 → A + x ∈ ℕ ↔ A + y + 1 ∈ ℕ
9 8 imbi2d ⊢ x = y + 1 → A ∈ ℕ → A + x ∈ ℕ ↔ A ∈ ℕ → A + y + 1 ∈ ℕ
10 oveq2 ⊢ x = B → A + x = A + B
11 10 eleq1d ⊢ x = B → A + x ∈ ℕ ↔ A + B ∈ ℕ
12 11 imbi2d ⊢ x = B → A ∈ ℕ → A + x ∈ ℕ ↔ A ∈ ℕ → A + B ∈ ℕ
13 peano2nn ⊢ A ∈ ℕ → A + 1 ∈ ℕ
14 peano2nn ⊢ A + y ∈ ℕ → A + y + 1 ∈ ℕ
15 nncn ⊢ A ∈ ℕ → A ∈ ℂ
16 nncn ⊢ y ∈ ℕ → y ∈ ℂ
17 ax-1cn ⊢ 1 ∈ ℂ
18 addass ⊢ A ∈ ℂ ∧ y ∈ ℂ ∧ 1 ∈ ℂ → A + y + 1 = A + y + 1
19 17 18 mp3an3 ⊢ A ∈ ℂ ∧ y ∈ ℂ → A + y + 1 = A + y + 1
20 15 16 19 syl2an ⊢ A ∈ ℕ ∧ y ∈ ℕ → A + y + 1 = A + y + 1
21 20 eleq1d ⊢ A ∈ ℕ ∧ y ∈ ℕ → A + y + 1 ∈ ℕ ↔ A + y + 1 ∈ ℕ
22 14 21 imbitrid ⊢ A ∈ ℕ ∧ y ∈ ℕ → A + y ∈ ℕ → A + y + 1 ∈ ℕ
23 22 expcom ⊢ y ∈ ℕ → A ∈ ℕ → A + y ∈ ℕ → A + y + 1 ∈ ℕ
24 23 a2d ⊢ y ∈ ℕ → A ∈ ℕ → A + y ∈ ℕ → A ∈ ℕ → A + y + 1 ∈ ℕ
25 3 6 9 12 13 24 nnind ⊢ B ∈ ℕ → A ∈ ℕ → A + B ∈ ℕ
26 25 impcom ⊢ A ∈ ℕ ∧ B ∈ ℕ → A + B ∈ ℕ