Theorem deccl 12648

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

Hypotheses

Ref	Expression
deccl.1	⊢ 𝐴 ∈ ℕ0
deccl.2	⊢ 𝐵 ∈ ℕ0

Assertion

Ref	Expression
deccl	⊢ ;𝐴𝐵 ∈ ℕ0

Proof of Theorem deccl

Step	Hyp	Ref	Expression
1		df-dec 12634	. 2 ⊢ ;𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵)
2		9nn0 12450	. . . 4 ⊢ 9 ∈ ℕ0
3		1nn0 12442	. . . 4 ⊢ 1 ∈ ℕ0
4	2, 3	nn0addcli 12463	. . 3 ⊢ (9 + 1) ∈ ℕ0
5		deccl.1	. . 3 ⊢ 𝐴 ∈ ℕ0
6		deccl.2	. . 3 ⊢ 𝐵 ∈ ℕ0
7	4, 5, 6	numcl 12646	. 2 ⊢ (((9 + 1) · 𝐴) + 𝐵) ∈ ℕ0
8	1, 7	eqeltri 2831	1 ⊢ ;𝐴𝐵 ∈ ℕ0

Syntax hints:   ∈ wcel 2114  (class class class)co 7356  1c1 11028   + caddc 11030   · cmul 11032  9c9 12232  ℕ₀cn0 12426  ;cdc 12633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7678  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3060  df-reu 3341  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-tr 5182  df-id 5515  df-eprel 5520  df-po 5528  df-so 5529  df-fr 5573  df-we 5575  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6254  df-ord 6315  df-on 6316  df-lim 6317  df-suc 6318  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-er 8632  df-en 8883  df-dom 8884  df-sdom 8885  df-pnf 11170  df-mnf 11171  df-ltxr 11173  df-nn 12164  df-2 12233  df-3 12234  df-4 12235  df-5 12236  df-6 12237  df-7 12238  df-8 12239  df-9 12240  df-n0 12427  df-dec 12634

This theorem is referenced by:  10nn0  12651  3declth  12665  3decltc  12666  decleh  12668  decmul1  12697  bpoly4  16013  fsumcube  16014  3dvds2dec  16291  dec2dvds  17023  dec5dvds2  17025  2exp8  17048  2exp11  17049  2exp16  17050  prmlem2  17079  37prm  17080  43prm  17081  83prm  17082  139prm  17083  163prm  17084  317prm  17085  631prm  17086  1259lem1  17090  1259lem2  17091  1259lem3  17092  1259lem4  17093  1259lem5  17094  1259prm  17095  2503lem1  17096  2503lem2  17097  2503lem3  17098  2503prm  17099  4001lem1  17100  4001lem2  17101  4001lem3  17102  4001lem4  17103  4001prm  17104  slotsbhcdif  17367  quart1cl  26806  quart1lem  26807  quart1  26808  log2ublem3  26900  log2ub  26901  log2le1  26902  birthday  26906  bpos1  27234  bpos  27244  1kp2ke3k  30504  9p10ne21  30528  dp3mul10  32945  dpmul1000  32946  dpadd  32958  dpmul  32960  dpmul4  32961  cos9thpiminplylem1  33914  hgt750lemd  34780  hgt750lem  34783  hgt750lem2  34784  hgt750leme  34790  tgoldbachgnn  34791  tgoldbachgt  34795  kur14lem9  35384  420gcd8e4  42433  12lcm5e60  42435  60lcm7e420  42437  3exp7  42480  3lexlogpow5ineq1  42481  3lexlogpow5ineq2  42482  3lexlogpow5ineq5  42487  aks4d1p1  42503  sqn5i  42705  decpmulnc  42707  decpmul  42708  sqdeccom12  42709  sq3deccom12  42710  235t711  42725  ex-decpmul  42726  sq45  43092  sum9cubes  43093  resqrtvalex  44060  imsqrtvalex  44061  inductionexd  44570  sin5tlem4  47312  sin5tlem5  47313  goldratmolem2  47322  fmtno3  48002  fmtno4  48003  fmtno5lem1  48004  fmtno5lem2  48005  fmtno5lem3  48006  fmtno5lem4  48007  fmtno5  48008  257prm  48012  fmtno4prmfac  48023  fmtno4nprmfac193  48025  fmtno5faclem1  48030  fmtno5faclem2  48031  fmtno5faclem3  48032  fmtno5fac  48033  fmtno5nprm  48034  139prmALT  48047  31prm  48048  127prm  48050  m7prm  48051  m11nprm  48052  11t31e341  48196  2exp340mod341  48197  341fppr2  48198  nfermltl2rev  48207  evengpoap3  48263  bgoldbachlt  48277  tgoldbachlt  48280  ackval3012  49156  ackval41a  49158  ackval41  49159  ackval42  49160