This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnacl

Description: Closure of addition of natural numbers. Proposition 8.9 of TakeutiZaring p. 59. Theorem 2.20 of Schloeder p. 6. (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 imbitrrid 
 |-  ( ( 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 )