Metamath Proof Explorer


Theorem nn0addcl

Description: Closure of addition of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002) (Proof shortened by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion nn0addcl M 0 N 0 M + N 0

Proof

Step Hyp Ref Expression
1 nnsscn
2 id
3 df-n0 0 = 0
4 nnaddcl M N M + N
5 4 adantl M N M + N
6 2 3 5 un0addcl M 0 N 0 M + N 0
7 1 6 mpan M 0 N 0 M + N 0