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 )