Theorem decnncl 12361

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

Hypotheses

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

Assertion

Ref	Expression
decnncl	⊢ ;𝐴𝐵 ∈ ℕ

Proof of Theorem decnncl

Step	Hyp	Ref	Expression
1		dfdec10 12344	. 2 ⊢ ;𝐴𝐵 = ((;10 · 𝐴) + 𝐵)
2		10nn0 12359	. . 3 ⊢ ;10 ∈ ℕ0
3		decnncl.1	. . 3 ⊢ 𝐴 ∈ ℕ0
4		decnncl.2	. . 3 ⊢ 𝐵 ∈ ℕ
5	2, 3, 4	numnncl 12351	. 2 ⊢ ((;10 · 𝐴) + 𝐵) ∈ ℕ
6	1, 5	eqeltri 2836	1 ⊢ ;𝐴𝐵 ∈ ℕ

Syntax hints:   ∈ wcel 2112  (class class class)co 7252  0cc0 10777  1c1 10778   + caddc 10780   · cmul 10782  ℕcn 11878  ℕ₀cn0 12138  ;cdc 12341

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5216  ax-nul 5223  ax-pow 5282  ax-pr 5346  ax-un 7563  ax-resscn 10834  ax-1cn 10835  ax-icn 10836  ax-addcl 10837  ax-addrcl 10838  ax-mulcl 10839  ax-mulrcl 10840  ax-mulcom 10841  ax-addass 10842  ax-mulass 10843  ax-distr 10844  ax-i2m1 10845  ax-1ne0 10846  ax-1rid 10847  ax-rnegex 10848  ax-rrecex 10849  ax-cnre 10850  ax-pre-lttri 10851  ax-pre-lttrn 10852  ax-pre-ltadd 10853

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3425  df-sbc 3713  df-csb 3830  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5153  df-tr 5186  df-id 5479  df-eprel 5485  df-po 5493  df-so 5494  df-fr 5534  df-we 5536  df-xp 5585  df-rel 5586  df-cnv 5587  df-co 5588  df-dm 5589  df-rn 5590  df-res 5591  df-ima 5592  df-pred 6189  df-ord 6251  df-on 6252  df-lim 6253  df-suc 6254  df-iota 6373  df-fun 6417  df-fn 6418  df-f 6419  df-f1 6420  df-fo 6421  df-f1o 6422  df-fv 6423  df-ov 7255  df-om 7685  df-wrecs 8089  df-recs 8150  df-rdg 8188  df-er 8433  df-en 8669  df-dom 8670  df-sdom 8671  df-pnf 10917  df-mnf 10918  df-ltxr 10920  df-nn 11879  df-2 11941  df-3 11942  df-4 11943  df-5 11944  df-6 11945  df-7 11946  df-8 11947  df-9 11948  df-n0 12139  df-dec 12342

This theorem is referenced by:  11prm  16719  13prm  16720  17prm  16721  19prm  16722  23prm  16723  37prm  16725  43prm  16726  83prm  16727  139prm  16728  163prm  16729  317prm  16730  631prm  16731  1259lem1  16735  1259lem2  16736  1259lem3  16737  1259lem4  16738  1259lem5  16739  1259prm  16740  2503lem1  16741  2503lem2  16742  2503lem3  16743  2503prm  16744  4001lem1  16745  4001lem2  16746  4001lem3  16747  4001lem4  16748  4001prm  16749  ocndx  16989  ocid  16990  dsndx  16991  dsid  16992  dsndxnn  16993  unifndx  17000  unifid  17001  unifndxnn  17002  odrngstr  17007  homndx  17015  homid  17016  ccondx  17017  ccoid  17018  imasvalstr  17054  prdsvalstr  17055  oppchomfvalOLD  17316  oppcbasOLD  17321  resccoOLD  17438  catstr  17565  ipostr  18137  mgpdsOLD  19624  sradsOLD  20344  cnfldstr  20487  tuslemOLD  23302  tmslemOLD  23519  mcubic  25877  cubic2  25878  cubic  25879  quart1cl  25884  quart1lem  25885  quart1  25886  quartlem1  25887  quartlem2  25888  log2ub  25979  log2le1  25980  birthday  25984  bposlem8  26319  bposlem9  26320  pntlemd  26622  pntlema  26624  pntlemb  26625  pntlemf  26633  pntlemo  26635  itvndx  26678  lngndx  26679  itvid  26680  lngid  26681  slotsinbpsd  26682  slotslnbpsd  26683  trkgstr  26684  ttgval  27115  ttglemOLD  27117  ttgdsOLD  27126  eengstr  27226  edgfid  27236  edgfndx  27237  edgfndxnn  27238  edgfndxidOLD  27240  baseltedgfOLD  27242  12gcd5e1  39918  60gcd7e1  39920  420gcd8e4  39921  12lcm5e60  39923  60lcm7e420  39925  420lcm8e840  39926  lcmineqlem  39967  3lexlogpow5ineq1  39969  3lexlogpow5ineq2  39970  3lexlogpow5ineq4  39971  3lexlogpow2ineq1  39973  3lexlogpow2ineq2  39974  3lexlogpow5ineq5  39975  aks4d1p1p5  39989  aks4d1p1  39990  257prm  44874  fmtno4prmfac  44885  fmtno4prmfac193  44886  fmtno4nprmfac193  44887  fmtno5nprm  44896  139prmALT  44909  127prm  44912  3exp4mod41  44929  41prothprmlem2  44931  2exp340mod341  45046  341fppr2  45047  bgoldbtbndlem1  45118  tgblthelfgott  45128  tgoldbachlt  45129  tgoldbach  45130