Theorem nnnn0d 12584

Description: A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnnn0d.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnnn0d	⊢ (𝜑 → 𝐴 ∈ ℕ0)

Proof of Theorem nnnn0d

Step	Hyp	Ref	Expression
1		nnssnn0 12526	. 2 ⊢ ℕ ⊆ ℕ0
2		nnnn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3992	1 ⊢ (𝜑 → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2105  ℕcn 12263  ℕ₀cn0 12523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-ss 3979  df-n0 12524

This theorem is referenced by:  nn0ge2m1nn0  12594  nnzd  12637  eluzge2nn0  12926  expgt1  14137  expaddzlem  14142  expaddz  14143  expmulz  14145  expmulnbnd  14270  exp11nnd  14296  facwordi  14324  faclbnd  14325  facavg  14336  bcm1k  14350  wrdeqs1cat  14754  cshwcsh2id  14863  relexpsucnnr  15060  isercolllem2  15698  bcxmas  15867  climcndslem1  15881  climcndslem2  15882  climcnds  15883  pwdif  15900  geo2sum  15905  mertenslem1  15916  prodmolem3  15965  prodmolem2a  15966  bpolydiflem  16086  eftabs  16107  efcllem  16109  eftlub  16141  eirrlem  16236  rpnnen2lem9  16254  rpnnen2lem11  16256  dvdsfac  16359  pwp1fsum  16424  oddpwp1fsum  16425  bitsfzo  16468  bitsfi  16470  sadcaddlem  16490  smumullem  16525  gcdcl  16539  dvdsgcdidd  16570  mulgcd  16581  rplpwr  16591  rprpwr  16592  rppwr  16593  nn0rppwr  16594  expgcd  16596  lcmcl  16634  lcmgcdnn  16644  lcmfcl  16661  nprmdvds1  16739  rpexp  16755  prmdvdsbc  16759  zsqrtelqelz  16791  phiprmpw  16809  eulerthlem2  16815  eulerth  16816  fermltl  16817  odzcllem  16825  odzdvds  16828  odzphi  16829  prm23lt5  16847  pythagtriplem6  16854  pythagtriplem7  16855  pcprmpw2  16915  dvdsprmpweqle  16919  pcprod  16928  pcfac  16932  pcbc  16933  expnprm  16935  pockthlem  16938  pockthg  16939  prmunb  16947  prmreclem2  16950  prmreclem3  16951  prmreclem4  16952  prmreclem5  16953  prmreclem6  16954  mul4sqlem  16986  4sqlem11  16988  4sqlem17  16994  vdwlem1  17014  vdwlem5  17018  vdwlem6  17019  vdwlem8  17021  vdwlem9  17022  vdwlem11  17024  vdwlem12  17025  vdwnnlem3  17030  ramz2  17057  ramub1lem1  17059  ramub1lem2  17060  ramub1  17061  prmgaplem3  17086  2expltfac  17126  psgnunilem3  19528  odfval  19564  mndodconglem  19573  gexcl3  19619  pgpfi1  19627  sylow1lem1  19630  gexexlem  19884  prmcyg  19926  gsumval3  19939  ablfacrplem  20099  ablfacrp  20100  ablfacrp2  20101  ablfac1eu  20107  prmgrpsimpgd  20148  srgbinomlem3  20245  srgbinomlem4  20246  fermltlchr  21561  freshmansdream  21610  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  cpmadugsumlemF  22897  ovoliunlem1  25550  mbfi1fseqlem1  25764  mbfi1fseqlem3  25766  mbfi1fseqlem5  25768  itg2cnlem2  25811  dvply1  26339  aalioulem2  26389  aalioulem5  26392  aaliou3lem1  26398  aaliou3lem2  26399  aaliou3lem8  26401  aaliou3lem6  26404  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  pserdvlem2  26486  cxpeq  26814  zrtelqelz  26815  dmgmdivn0  27085  lgamgulmlem5  27090  lgamcvg2  27112  wilthlem1  27125  ftalem1  27130  ftalem2  27131  ftalem4  27133  ftalem5  27134  basellem2  27139  basellem3  27140  basellem4  27141  basellem5  27142  isppw2  27172  mpodvdsmulf1o  27251  dvdsmulf1o  27253  sgmmul  27259  fsumvma2  27272  chpchtsum  27277  logfacubnd  27279  mersenne  27285  perfect1  27286  perfectlem1  27287  perfectlem2  27288  perfect  27289  dchrelbas3  27296  dchrelbasd  27297  dchrzrh1  27302  dchrzrhmul  27304  dchrmulcl  27307  dchrn0  27308  dchrfi  27313  dchrghm  27314  dchrabs  27318  dchrinv  27319  dchrptlem1  27322  dchrptlem2  27323  dchrptlem3  27324  dchrpt  27325  dchrsum2  27326  sum2dchr  27332  pcbcctr  27334  bcmono  27335  bclbnd  27338  bposlem1  27342  bposlem3  27344  bposlem5  27346  bposlem6  27347  lgslem1  27355  lgsval2lem  27365  lgsvalmod  27374  lgsmod  27381  lgsdirprm  27389  lgsne0  27393  lgsqrlem1  27404  lgsqrlem2  27405  lgsqrlem3  27406  lgsqrlem4  27407  gausslemma2dlem0b  27415  gausslemma2dlem0c  27416  gausslemma2dlem1  27424  gausslemma2dlem7  27431  gausslemma2d  27432  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem3  27435  lgseisenlem4  27436  lgseisen  27437  lgsquadlem2  27439  lgsquadlem3  27440  m1lgs  27446  2lgslem1a  27449  2sqlem3  27478  2sqblem  27489  chebbnd1lem1  27527  chebbnd1lem3  27529  rplogsumlem2  27543  rpvmasumlem  27545  dchrisumlem1  27547  dchrisumlem2  27548  dchrmusum2  27552  dchrvmasumlem3  27557  dchrisum0ff  27565  dchrisum0flblem1  27566  rpvmasum2  27570  dchrisum0re  27571  dchrisum0lem2a  27575  dirith  27587  mudivsum  27588  pntpbnd1a  27643  pntlemq  27659  pntlemr  27660  pntlemj  27661  ostth2lem1  27676  ostth2lem2  27692  ostth2lem3  27693  ostth2  27695  crctcshwlkn0lem6  29844  hashecclwwlkn1  30105  umgrhashecclwwlk  30106  clwwlknon  30118  eucrctshift  30271  numclwlk1lem2  30398  nrt2irr  30501  dipcl  30740  dipcn  30748  bcm1n  32802  expgt0b  32822  wrdpmtrlast  33095  psgnfzto1st  33107  isarchi2  33174  submarchi  33175  znfermltl  33373  submateqlem1  33767  madjusmdetlem2  33788  madjusmdetlem4  33790  mdetlap  33792  nexple  33989  oddpwdc  34335  eulerpartlemsv2  34339  eulerpartlemsf  34340  eulerpartlems  34341  eulerpartlemv  34345  eulerpartlemb  34349  plymulx0  34540  signsvtn0  34563  fsum2dsub  34600  reprinfz1  34615  reprpmtf1o  34619  circlemeth  34633  circlemethnat  34634  hgt750lemb  34649  hgt750lema  34650  hgt750leme  34651  tgoldbachgtde  34653  tgoldbachgtda  34654  lpadleft  34676  subfacp1lem1  35163  subfacp1lem6  35169  subfaclim  35172  erdszelem8  35182  erdszelem10  35184  cvmliftlem10  35278  faclim2  35727  poimirlem7  37613  poimirlem17  37623  poimirlem18  37624  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  poimirlem28  37634  poimirlem32  37638  nninfnub  37737  bfplem1  37808  zndvdchrrhm  41952  lcmineqlem1  42010  lcmineqlem2  42011  lcmineqlem8  42017  lcmineqlem10  42019  lcmineqlem11  42020  lcmineqlem15  42024  lcmineqlem16  42025  lcmineqlem18  42027  lcmineqlem19  42028  lcmineqlem20  42029  lcmineqlem21  42030  lcmineqlem22  42031  3lexlogpow2ineq2  42040  dvrelogpow2b  42049  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1  42057  aks4d1p3  42059  aks4d1p7d1  42063  aks4d1p7  42064  aks4d1p8  42068  aks4d1p9  42069  isprimroot2  42075  primrootsunit1  42078  primrootscoprmpow  42080  posbezout  42081  primrootscoprbij  42083  primrootlekpowne0  42086  primrootspoweq0  42087  aks6d1c1p2  42090  aks6d1c1p3  42091  aks6d1c1p4  42092  aks6d1c1p5  42093  aks6d1c1p7  42094  aks6d1c1p6  42095  aks6d1c1p8  42096  aks6d1c2p2  42100  hashscontpowcl  42101  hashscontpow1  42102  hashscontpow  42103  aks6d1c4  42105  aks6d1c2lem3  42107  aks6d1c2lem4  42108  aks6d1c2  42111  sticksstones6  42132  sticksstones7  42133  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  sticksstones20  42147  sticksstones22  42149  aks6d1c6lem2  42152  aks6d1c6lem3  42153  aks6d1c6lem4  42154  aks6d1c6isolem1  42155  aks6d1c6isolem2  42156  aks6d1c6lem5  42158  bcled  42159  bcle2d  42160  aks6d1c7lem1  42161  aks6d1c7  42165  aks5lem2  42168  aks5lem3a  42170  aks5lem5a  42172  grpods  42175  unitscyglem2  42177  unitscyglem4  42179  aks5lem7  42181  aks5  42185  metakunt2  42187  sumcubes  42325  oexpreposd  42335  exp11d  42339  dvdsexpb  42348  fiabv  42522  fsuppind  42576  dffltz  42620  fltdvdsabdvdsc  42624  fltne  42630  flt4lem4  42635  flt4lem7  42645  fltltc  42647  fltnltalem  42648  fltnlta  42649  3rexfrabdioph  42784  4rexfrabdioph  42785  6rexfrabdioph  42786  7rexfrabdioph  42787  irrapxlem5  42813  pellexlem2  42817  pellexlem6  42821  pell14qrgt0  42846  pell1qrge1  42857  pellfundgt1  42870  ltrmxnn0  42937  jm2.26lem3  42989  jm2.27a  42993  jm2.27c  42995  rmxdiophlem  43003  jm3.1lem1  43005  jm3.1lem2  43006  jm3.1lem3  43007  jm3.1  43008  dgrsub2  43123  mpaaeu  43138  idomsubgmo  43181  relexpxpmin  43706  nzprmdif  44314  binomcxplemwb  44343  fperiodmul  45254  xralrple4  45322  fsumnncl  45527  dvsinexp  45866  dvxpaek  45895  itgsinexplem1  45909  stoweidlem1  45956  stoweidlem17  45972  stoweidlem25  45980  stoweidlem34  45989  stoweidlem38  45993  stoweidlem40  45995  stoweidlem42  45997  stoweidlem45  46000  stirlinglem4  46032  stirlinglem5  46033  stirlinglem10  46038  stirlinglem13  46041  dirkertrigeq  46056  fourierdlem21  46083  fourierdlem25  46087  fourierdlem48  46109  fourierdlem54  46115  fourierdlem64  46125  fourierdlem65  46126  fourierdlem73  46134  fourierdlem81  46142  fourierdlem83  46144  fourierdlem92  46153  fourierdlem103  46164  fourierdlem104  46165  fourierdlem112  46173  fourierdlem113  46174  etransclem1  46190  etransclem4  46193  etransclem8  46197  etransclem15  46204  etransclem17  46206  etransclem18  46207  etransclem19  46208  etransclem20  46209  etransclem21  46210  etransclem22  46211  etransclem23  46212  etransclem24  46213  etransclem25  46214  etransclem27  46216  etransclem32  46221  etransclem35  46224  etransclem41  46230  etransclem44  46233  etransclem46  46235  iccpartigtl  47347  iccpartgt  47351  iccpartgel  47353  iccelpart  47357  odz2prm2pw  47487  fmtnoprmfac1  47489  fmtnoprmfac2  47491  2pwp1prm  47513  sfprmdvdsmersenne  47527  lighneallem4a  47532  proththdlem  47537  proththd  47538  perfectALTVlem1  47645  perfectALTVlem2  47646  perfectALTV  47647  fpprwpprb  47664  gpgedgvtx1  47954  gpg3nbgrvtxlem  47957  logbpw2m1  48416  nnpw2blenfzo  48430  nnolog2flm1  48439  dignn0fr  48450  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469