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	imbitrid	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( ( 𝐴 + 𝑦 ) ∈ ℕ → ( 𝐴 + ( 𝑦 + 1 ) ) ∈ ℕ ) )
23	22	expcom	⊢ ( 𝑦 ∈ ℕ → ( 𝐴 ∈ ℕ → ( ( 𝐴 + 𝑦 ) ∈ ℕ → ( 𝐴 + ( 𝑦 + 1 ) ) ∈ ℕ ) ) )
24	23	a2d	⊢ ( 𝑦 ∈ ℕ → ( ( 𝐴 ∈ ℕ → ( 𝐴 + 𝑦 ) ∈ ℕ ) → ( 𝐴 ∈ ℕ → ( 𝐴 + ( 𝑦 + 1 ) ) ∈ ℕ ) ) )
25	3 6 9 12 13 24	nnind	⊢ ( 𝐵 ∈ ℕ → ( 𝐴 ∈ ℕ → ( 𝐴 + 𝐵 ) ∈ ℕ ) )
26	25	impcom	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 + 𝐵 ) ∈ ℕ )

Metamath Proof Explorer

Theorem nnaddcl

Proof