# Metamath Proof Explorer

## Theorem nnacl

Description: Closure of addition of natural numbers. Proposition 8.9 of TakeutiZaring p. 59. (Contributed by NM, 20-Sep-1995) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion nnacl ${⊢}\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\to {A}{+}_{𝑜}{B}\in \mathrm{\omega }$

### Proof

Step Hyp Ref Expression
1 oveq2 ${⊢}{x}={B}\to {A}{+}_{𝑜}{x}={A}{+}_{𝑜}{B}$
2 1 eleq1d ${⊢}{x}={B}\to \left({A}{+}_{𝑜}{x}\in \mathrm{\omega }↔{A}{+}_{𝑜}{B}\in \mathrm{\omega }\right)$
3 2 imbi2d ${⊢}{x}={B}\to \left(\left({A}\in \mathrm{\omega }\to {A}{+}_{𝑜}{x}\in \mathrm{\omega }\right)↔\left({A}\in \mathrm{\omega }\to {A}{+}_{𝑜}{B}\in \mathrm{\omega }\right)\right)$
4 oveq2 ${⊢}{x}=\varnothing \to {A}{+}_{𝑜}{x}={A}{+}_{𝑜}\varnothing$
5 4 eleq1d ${⊢}{x}=\varnothing \to \left({A}{+}_{𝑜}{x}\in \mathrm{\omega }↔{A}{+}_{𝑜}\varnothing \in \mathrm{\omega }\right)$
6 oveq2 ${⊢}{x}={y}\to {A}{+}_{𝑜}{x}={A}{+}_{𝑜}{y}$
7 6 eleq1d ${⊢}{x}={y}\to \left({A}{+}_{𝑜}{x}\in \mathrm{\omega }↔{A}{+}_{𝑜}{y}\in \mathrm{\omega }\right)$
8 oveq2 ${⊢}{x}=\mathrm{suc}{y}\to {A}{+}_{𝑜}{x}={A}{+}_{𝑜}\mathrm{suc}{y}$
9 8 eleq1d ${⊢}{x}=\mathrm{suc}{y}\to \left({A}{+}_{𝑜}{x}\in \mathrm{\omega }↔{A}{+}_{𝑜}\mathrm{suc}{y}\in \mathrm{\omega }\right)$
10 nna0 ${⊢}{A}\in \mathrm{\omega }\to {A}{+}_{𝑜}\varnothing ={A}$
11 10 eleq1d ${⊢}{A}\in \mathrm{\omega }\to \left({A}{+}_{𝑜}\varnothing \in \mathrm{\omega }↔{A}\in \mathrm{\omega }\right)$
12 11 ibir ${⊢}{A}\in \mathrm{\omega }\to {A}{+}_{𝑜}\varnothing \in \mathrm{\omega }$
13 peano2 ${⊢}{A}{+}_{𝑜}{y}\in \mathrm{\omega }\to \mathrm{suc}\left({A}{+}_{𝑜}{y}\right)\in \mathrm{\omega }$
14 nnasuc ${⊢}\left({A}\in \mathrm{\omega }\wedge {y}\in \mathrm{\omega }\right)\to {A}{+}_{𝑜}\mathrm{suc}{y}=\mathrm{suc}\left({A}{+}_{𝑜}{y}\right)$
15 14 eleq1d ${⊢}\left({A}\in \mathrm{\omega }\wedge {y}\in \mathrm{\omega }\right)\to \left({A}{+}_{𝑜}\mathrm{suc}{y}\in \mathrm{\omega }↔\mathrm{suc}\left({A}{+}_{𝑜}{y}\right)\in \mathrm{\omega }\right)$
16 13 15 syl5ibr ${⊢}\left({A}\in \mathrm{\omega }\wedge {y}\in \mathrm{\omega }\right)\to \left({A}{+}_{𝑜}{y}\in \mathrm{\omega }\to {A}{+}_{𝑜}\mathrm{suc}{y}\in \mathrm{\omega }\right)$
17 16 expcom ${⊢}{y}\in \mathrm{\omega }\to \left({A}\in \mathrm{\omega }\to \left({A}{+}_{𝑜}{y}\in \mathrm{\omega }\to {A}{+}_{𝑜}\mathrm{suc}{y}\in \mathrm{\omega }\right)\right)$
18 5 7 9 12 17 finds2 ${⊢}{x}\in \mathrm{\omega }\to \left({A}\in \mathrm{\omega }\to {A}{+}_{𝑜}{x}\in \mathrm{\omega }\right)$
19 3 18 vtoclga ${⊢}{B}\in \mathrm{\omega }\to \left({A}\in \mathrm{\omega }\to {A}{+}_{𝑜}{B}\in \mathrm{\omega }\right)$
20 19 impcom ${⊢}\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\to {A}{+}_{𝑜}{B}\in \mathrm{\omega }$