Metamath Proof Explorer

Theorem deccl

Description: Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 6-Sep-2021)

Ref Expression
Hypotheses deccl.1 
|- A e. NN0
deccl.2 
|- B e. NN0
Assertion deccl 
|- ; A B e. NN0

Proof

Step Hyp Ref Expression
1 deccl.1 
 |-  A e. NN0
2 deccl.2 
 |-  B e. NN0
3 df-dec 
 |-  ; A B = ( ( ( 9 + 1 ) x. A ) + B )
4 9nn0 
 |-  9 e. NN0
5 1nn0 
 |-  1 e. NN0
6 4 5 nn0addcli 
 |-  ( 9 + 1 ) e. NN0
7 6 1 2 numcl 
 |-  ( ( ( 9 + 1 ) x. A ) + B ) e. NN0
8 3 7 eqeltri 
 |-  ; A B e. NN0