Metamath Proof Explorer

Theorem decnncl2

Description: Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 6-Sep-2021)

Ref Expression
Hypothesis decnncl2.1 
|- A e. NN
Assertion decnncl2 
|- ; A 0 e. NN

Proof

Step Hyp Ref Expression
1 decnncl2.1 
 |-  A e. NN
2 dfdec10 
 |-  ; A 0 = ( ( ; 1 0 x. A ) + 0 )
3 10nn 
 |-  ; 1 0 e. NN
4 3 1 numnncl2 
 |-  ( ( ; 1 0 x. A ) + 0 ) e. NN
5 2 4 eqeltri 
 |-  ; A 0 e. NN