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∈ℕ