# 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
`|- ( ( A e. _om /\ B e. _om ) -> ( A +o B ) e. _om )`

### Proof

Step Hyp Ref Expression
1 oveq2
` |-  ( x = B -> ( A +o x ) = ( A +o B ) )`
2 1 eleq1d
` |-  ( x = B -> ( ( A +o x ) e. _om <-> ( A +o B ) e. _om ) )`
3 2 imbi2d
` |-  ( x = B -> ( ( A e. _om -> ( A +o x ) e. _om ) <-> ( A e. _om -> ( A +o B ) e. _om ) ) )`
4 oveq2
` |-  ( x = (/) -> ( A +o x ) = ( A +o (/) ) )`
5 4 eleq1d
` |-  ( x = (/) -> ( ( A +o x ) e. _om <-> ( A +o (/) ) e. _om ) )`
6 oveq2
` |-  ( x = y -> ( A +o x ) = ( A +o y ) )`
7 6 eleq1d
` |-  ( x = y -> ( ( A +o x ) e. _om <-> ( A +o y ) e. _om ) )`
8 oveq2
` |-  ( x = suc y -> ( A +o x ) = ( A +o suc y ) )`
9 8 eleq1d
` |-  ( x = suc y -> ( ( A +o x ) e. _om <-> ( A +o suc y ) e. _om ) )`
10 nna0
` |-  ( A e. _om -> ( A +o (/) ) = A )`
11 10 eleq1d
` |-  ( A e. _om -> ( ( A +o (/) ) e. _om <-> A e. _om ) )`
12 11 ibir
` |-  ( A e. _om -> ( A +o (/) ) e. _om )`
13 peano2
` |-  ( ( A +o y ) e. _om -> suc ( A +o y ) e. _om )`
14 nnasuc
` |-  ( ( A e. _om /\ y e. _om ) -> ( A +o suc y ) = suc ( A +o y ) )`
15 14 eleq1d
` |-  ( ( A e. _om /\ y e. _om ) -> ( ( A +o suc y ) e. _om <-> suc ( A +o y ) e. _om ) )`
16 13 15 syl5ibr
` |-  ( ( A e. _om /\ y e. _om ) -> ( ( A +o y ) e. _om -> ( A +o suc y ) e. _om ) )`
17 16 expcom
` |-  ( y e. _om -> ( A e. _om -> ( ( A +o y ) e. _om -> ( A +o suc y ) e. _om ) ) )`
18 5 7 9 12 17 finds2
` |-  ( x e. _om -> ( A e. _om -> ( A +o x ) e. _om ) )`
19 3 18 vtoclga
` |-  ( B e. _om -> ( A e. _om -> ( A +o B ) e. _om ) )`
20 19 impcom
` |-  ( ( A e. _om /\ B e. _om ) -> ( A +o B ) e. _om )`