Theorem deccl 12633

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 12619	. 2 ⊢ ;𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵)
2		9nn0 12437	. . . 4 ⊢ 9 ∈ ℕ0
3		1nn0 12429	. . . 4 ⊢ 1 ∈ ℕ0
4	2, 3	nn0addcli 12450	. . 3 ⊢ (9 + 1) ∈ ℕ0
5		deccl.1	. . 3 ⊢ 𝐴 ∈ ℕ0
6		deccl.2	. . 3 ⊢ 𝐵 ∈ ℕ0
7	4, 5, 6	numcl 12631	. 2 ⊢ (((9 + 1) · 𝐴) + 𝐵) ∈ ℕ0
8	1, 7	eqeltri 2834	1 ⊢ ;𝐴𝐵 ∈ ℕ0

Syntax hints:   ∈ wcel 2106  (class class class)co 7357  1c1 11052   + caddc 11054   · cmul 11056  9c9 12215  ℕ₀cn0 12413  ;cdc 12618

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-ltxr 11194  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-dec 12619

This theorem is referenced by:  10nn0  12636  3declth  12650  3decltc  12651  decleh  12653  decmul1  12682  bpoly4  15942  fsumcube  15943  3dvds2dec  16215  dec2dvds  16935  dec5dvds2  16937  2exp8  16961  2exp11  16962  2exp16  16963  prmlem2  16992  37prm  16993  43prm  16994  83prm  16995  139prm  16996  163prm  16997  317prm  16998  631prm  16999  1259lem1  17003  1259lem2  17004  1259lem3  17005  1259lem4  17006  1259lem5  17007  1259prm  17008  2503lem1  17009  2503lem2  17010  2503lem3  17011  2503prm  17012  4001lem1  17013  4001lem2  17014  4001lem3  17015  4001lem4  17016  4001prm  17017  slotsbhcdif  17296  slotsbhcdifOLD  17297  cnfldfunALTOLD  20810  tnglemOLD  23997  quart1cl  26204  quart1lem  26205  quart1  26206  log2ublem3  26298  log2ub  26299  log2le1  26300  birthday  26304  bpos1  26631  bpos  26641  1kp2ke3k  29390  9p10ne21  29414  dp3mul10  31754  dpmul1000  31755  dpadd  31767  dpmul  31769  dpmul4  31770  hgt750lemd  33261  hgt750lem  33264  hgt750lem2  33265  hgt750leme  33271  tgoldbachgnn  33272  tgoldbachgt  33276  kur14lem9  33808  420gcd8e4  40463  12lcm5e60  40465  60lcm7e420  40467  3exp7  40510  3lexlogpow5ineq1  40511  3lexlogpow5ineq2  40512  3lexlogpow5ineq5  40517  aks4d1p1  40533  sqn5i  40785  decpmulnc  40787  decpmul  40788  sqdeccom12  40789  sq3deccom12  40790  235t711  40791  ex-decpmul  40792  resqrtvalex  41907  imsqrtvalex  41908  inductionexd  42417  fmtno3  45733  fmtno4  45734  fmtno5lem1  45735  fmtno5lem2  45736  fmtno5lem3  45737  fmtno5lem4  45738  fmtno5  45739  257prm  45743  fmtno4prmfac  45754  fmtno4nprmfac193  45756  fmtno5faclem1  45761  fmtno5faclem2  45762  fmtno5faclem3  45763  fmtno5fac  45764  fmtno5nprm  45765  139prmALT  45778  31prm  45779  127prm  45781  m7prm  45782  m11nprm  45783  11t31e341  45914  2exp340mod341  45915  341fppr2  45916  nfermltl2rev  45925  evengpoap3  45981  bgoldbachlt  45995  tgoldbachlt  45998  ackval3012  46768  ackval41a  46770  ackval41  46771  ackval42  46772  prstcocvalOLD  47082