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 ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 + 𝐵 ) ∈ ℕ )

Proof

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