Metamath Proof Explorer

Theorem nnaddm1cl

Description: Closure of addition of positive integers minus one. (Contributed by NM, 6-Aug-2003) (Proof shortened by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion nnaddm1cl 
|- ( ( A e. NN /\ B e. NN ) -> ( ( A + B ) - 1 ) e. NN )

Proof

Step Hyp Ref Expression
1 nncn 
 |-  ( A e. NN -> A e. CC )
2 nncn 
 |-  ( B e. NN -> B e. CC )
3 ax-1cn 
 |-  1 e. CC
4 addsub 
 |-  ( ( A e. CC /\ B e. CC /\ 1 e. CC ) -> ( ( A + B ) - 1 ) = ( ( A - 1 ) + B ) )
5 3 4 mp3an3 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - 1 ) = ( ( A - 1 ) + B ) )
6 1 2 5 syl2an 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A + B ) - 1 ) = ( ( A - 1 ) + B ) )
7 nnm1nn0 
 |-  ( A e. NN -> ( A - 1 ) e. NN0 )
8 nn0nnaddcl 
 |-  ( ( ( A - 1 ) e. NN0 /\ B e. NN ) -> ( ( A - 1 ) + B ) e. NN )
9 7 8 sylan 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A - 1 ) + B ) e. NN )
10 6 9 eqeltrd 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( A + B ) - 1 ) e. NN )