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

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 
|- ( ( A e. NN /\ B e. NN ) -> ( A + B ) e. NN )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = 1 -> ( A + x ) = ( A + 1 ) )
2 1 eleq1d 
 |-  ( x = 1 -> ( ( A + x ) e. NN <-> ( A + 1 ) e. NN ) )
3 2 imbi2d 
 |-  ( x = 1 -> ( ( A e. NN -> ( A + x ) e. NN ) <-> ( A e. NN -> ( A + 1 ) e. NN ) ) )
4 oveq2 
 |-  ( x = y -> ( A + x ) = ( A + y ) )
5 4 eleq1d 
 |-  ( x = y -> ( ( A + x ) e. NN <-> ( A + y ) e. NN ) )
6 5 imbi2d 
 |-  ( x = y -> ( ( A e. NN -> ( A + x ) e. NN ) <-> ( A e. NN -> ( A + y ) e. NN ) ) )
7 oveq2 
 |-  ( x = ( y + 1 ) -> ( A + x ) = ( A + ( y + 1 ) ) )
8 7 eleq1d 
 |-  ( x = ( y + 1 ) -> ( ( A + x ) e. NN <-> ( A + ( y + 1 ) ) e. NN ) )
9 8 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( A e. NN -> ( A + x ) e. NN ) <-> ( A e. NN -> ( A + ( y + 1 ) ) e. NN ) ) )
10 oveq2 
 |-  ( x = B -> ( A + x ) = ( A + B ) )
11 10 eleq1d 
 |-  ( x = B -> ( ( A + x ) e. NN <-> ( A + B ) e. NN ) )
12 11 imbi2d 
 |-  ( x = B -> ( ( A e. NN -> ( A + x ) e. NN ) <-> ( A e. NN -> ( A + B ) e. NN ) ) )
13 peano2nn 
 |-  ( A e. NN -> ( A + 1 ) e. NN )
14 peano2nn 
 |-  ( ( A + y ) e. NN -> ( ( A + y ) + 1 ) e. NN )
15 nncn 
 |-  ( A e. NN -> A e. CC )
16 nncn 
 |-  ( y e. NN -> y e. CC )
17 ax-1cn 
 |-  1 e. CC
18 addass 
 |-  ( ( A e. CC /\ y e. CC /\ 1 e. CC ) -> ( ( A + y ) + 1 ) = ( A + ( y + 1 ) ) )
19 17 18 mp3an3 
 |-  ( ( A e. CC /\ y e. CC ) -> ( ( A + y ) + 1 ) = ( A + ( y + 1 ) ) )
20 15 16 19 syl2an 
 |-  ( ( A e. NN /\ y e. NN ) -> ( ( A + y ) + 1 ) = ( A + ( y + 1 ) ) )
21 20 eleq1d 
 |-  ( ( A e. NN /\ y e. NN ) -> ( ( ( A + y ) + 1 ) e. NN <-> ( A + ( y + 1 ) ) e. NN ) )
22 14 21 imbitrid 
 |-  ( ( A e. NN /\ y e. NN ) -> ( ( A + y ) e. NN -> ( A + ( y + 1 ) ) e. NN ) )
23 22 expcom 
 |-  ( y e. NN -> ( A e. NN -> ( ( A + y ) e. NN -> ( A + ( y + 1 ) ) e. NN ) ) )
24 23 a2d 
 |-  ( y e. NN -> ( ( A e. NN -> ( A + y ) e. NN ) -> ( A e. NN -> ( A + ( y + 1 ) ) e. NN ) ) )
25 3 6 9 12 13 24 nnind 
 |-  ( B e. NN -> ( A e. NN -> ( A + B ) e. NN ) )
26 25 impcom 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A + B ) e. NN )