Metamath Proof Explorer


Theorem numnncl2

Description: Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 9-Mar-2015)

Ref Expression
Hypotheses numnncl2.1
|- T e. NN
numnncl2.2
|- A e. NN
Assertion numnncl2
|- ( ( T x. A ) + 0 ) e. NN

Proof

Step Hyp Ref Expression
1 numnncl2.1
 |-  T e. NN
2 numnncl2.2
 |-  A e. NN
3 1 2 nnmulcli
 |-  ( T x. A ) e. NN
4 3 nncni
 |-  ( T x. A ) e. CC
5 4 addid1i
 |-  ( ( T x. A ) + 0 ) = ( T x. A )
6 5 3 eqeltri
 |-  ( ( T x. A ) + 0 ) e. NN