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

Metamath Proof Explorer

Theorem nnnn0addcl

Description: A positive integer plus a nonnegative integer is a positive integer. (Contributed by NM, 20-Apr-2005) (Proof shortened by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion nnnn0addcl 
|- ( ( M e. NN /\ N e. NN0 ) -> ( M + N ) e. NN )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 nnaddcl 
 |-  ( ( M e. NN /\ N e. NN ) -> ( M + N ) e. NN )
3 oveq2 
 |-  ( N = 0 -> ( M + N ) = ( M + 0 ) )
4 nncn 
 |-  ( M e. NN -> M e. CC )
5 4 addridd 
 |-  ( M e. NN -> ( M + 0 ) = M )
6 3 5 sylan9eqr 
 |-  ( ( M e. NN /\ N = 0 ) -> ( M + N ) = M )
7 simpl 
 |-  ( ( M e. NN /\ N = 0 ) -> M e. NN )
8 6 7 eqeltrd 
 |-  ( ( M e. NN /\ N = 0 ) -> ( M + N ) e. NN )
9 2 8 jaodan 
 |-  ( ( M e. NN /\ ( N e. NN \/ N = 0 ) ) -> ( M + N ) e. NN )
10 1 9 sylan2b 
 |-  ( ( M e. NN /\ N e. NN0 ) -> ( M + N ) e. NN )