Theorem nnnn0d 12437

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 12379	. 2 ⊢ ℕ ⊆ ℕ0
2		nnnn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3927	1 ⊢ (𝜑 → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2111  ℕcn 12120  ℕ₀cn0 12376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-ss 3914  df-n0 12377

This theorem is referenced by:  nn0ge2m1nn0  12447  nnzd  12490  eluzge2nn0  12785  expgt1  14002  expaddzlem  14007  expaddz  14008  expmulz  14010  expmulnbnd  14137  exp11nnd  14163  facwordi  14191  faclbnd  14192  facavg  14203  bcm1k  14217  wrdeqs1cat  14622  cshwcsh2id  14730  relexpsucnnr  14927  isercolllem2  15568  bcxmas  15737  climcndslem1  15751  climcndslem2  15752  climcnds  15753  pwdif  15770  geo2sum  15775  mertenslem1  15786  prodmolem3  15835  prodmolem2a  15836  bpolydiflem  15956  eftabs  15977  efcllem  15979  eftlub  16013  eirrlem  16108  rpnnen2lem9  16126  rpnnen2lem11  16128  dvdsfac  16232  pwp1fsum  16297  oddpwp1fsum  16298  bitsfzo  16341  bitsfi  16343  sadcaddlem  16363  smumullem  16398  gcdcl  16412  dvdsgcdidd  16443  mulgcd  16454  rplpwr  16464  rprpwr  16465  rppwr  16466  nn0rppwr  16467  expgcd  16469  lcmcl  16507  lcmgcdnn  16517  lcmfcl  16534  nprmdvds1  16612  rpexp  16628  prmdvdsbc  16632  zsqrtelqelz  16664  phiprmpw  16682  eulerthlem2  16688  eulerth  16689  fermltl  16690  odzcllem  16699  odzdvds  16702  odzphi  16703  prm23lt5  16721  pythagtriplem6  16728  pythagtriplem7  16729  pcprmpw2  16789  dvdsprmpweqle  16793  pcprod  16802  pcfac  16806  pcbc  16807  expnprm  16809  pockthlem  16812  pockthg  16813  prmunb  16821  prmreclem2  16824  prmreclem3  16825  prmreclem4  16826  prmreclem5  16827  prmreclem6  16828  mul4sqlem  16860  4sqlem11  16862  4sqlem17  16868  vdwlem1  16888  vdwlem5  16892  vdwlem6  16893  vdwlem8  16895  vdwlem9  16896  vdwlem11  16898  vdwlem12  16899  vdwnnlem3  16904  ramz2  16931  ramub1lem1  16933  ramub1lem2  16934  ramub1  16935  prmgaplem3  16960  2expltfac  16999  psgnunilem3  19403  odfval  19439  mndodconglem  19448  gexcl3  19494  pgpfi1  19502  sylow1lem1  19505  gexexlem  19759  prmcyg  19801  gsumval3  19814  ablfacrplem  19974  ablfacrp  19975  ablfacrp2  19976  ablfac1eu  19982  prmgrpsimpgd  20023  srgbinomlem3  20141  srgbinomlem4  20142  fermltlchr  21461  freshmansdream  21506  chfacfscmulgsum  22770  chfacfpmmulgsum  22774  cpmadugsumlemF  22786  ovoliunlem1  25425  mbfi1fseqlem1  25638  mbfi1fseqlem3  25640  mbfi1fseqlem5  25642  itg2cnlem2  25685  dvply1  26213  aalioulem2  26263  aalioulem5  26266  aaliou3lem1  26272  aaliou3lem2  26273  aaliou3lem8  26275  aaliou3lem6  26278  taylthlem1  26303  taylthlem2  26304  taylthlem2OLD  26305  pserdvlem2  26360  cxpeq  26689  zrtelqelz  26690  dmgmdivn0  26960  lgamgulmlem5  26965  lgamcvg2  26987  wilthlem1  27000  ftalem1  27005  ftalem2  27006  ftalem4  27008  ftalem5  27009  basellem2  27014  basellem3  27015  basellem4  27016  basellem5  27017  isppw2  27047  mpodvdsmulf1o  27126  dvdsmulf1o  27128  sgmmul  27134  fsumvma2  27147  chpchtsum  27152  logfacubnd  27154  mersenne  27160  perfect1  27161  perfectlem1  27162  perfectlem2  27163  perfect  27164  dchrelbas3  27171  dchrelbasd  27172  dchrzrh1  27177  dchrzrhmul  27179  dchrmulcl  27182  dchrn0  27183  dchrfi  27188  dchrghm  27189  dchrabs  27193  dchrinv  27194  dchrptlem1  27197  dchrptlem2  27198  dchrptlem3  27199  dchrpt  27200  dchrsum2  27201  sum2dchr  27207  pcbcctr  27209  bcmono  27210  bclbnd  27213  bposlem1  27217  bposlem3  27219  bposlem5  27221  bposlem6  27222  lgslem1  27230  lgsval2lem  27240  lgsvalmod  27249  lgsmod  27256  lgsdirprm  27264  lgsne0  27268  lgsqrlem1  27279  lgsqrlem2  27280  lgsqrlem3  27281  lgsqrlem4  27282  gausslemma2dlem0b  27290  gausslemma2dlem0c  27291  gausslemma2dlem1  27299  gausslemma2dlem7  27306  gausslemma2d  27307  lgseisenlem1  27308  lgseisenlem2  27309  lgseisenlem3  27310  lgseisenlem4  27311  lgseisen  27312  lgsquadlem2  27314  lgsquadlem3  27315  m1lgs  27321  2lgslem1a  27324  2sqlem3  27353  2sqblem  27364  chebbnd1lem1  27402  chebbnd1lem3  27404  rplogsumlem2  27418  rpvmasumlem  27420  dchrisumlem1  27422  dchrisumlem2  27423  dchrmusum2  27427  dchrvmasumlem3  27432  dchrisum0ff  27440  dchrisum0flblem1  27441  rpvmasum2  27445  dchrisum0re  27446  dchrisum0lem2a  27450  dirith  27462  mudivsum  27463  pntpbnd1a  27518  pntlemq  27534  pntlemr  27535  pntlemj  27536  ostth2lem1  27551  ostth2lem2  27567  ostth2lem3  27568  ostth2  27570  crctcshwlkn0lem6  29788  hashecclwwlkn1  30049  umgrhashecclwwlk  30050  clwwlknon  30062  eucrctshift  30215  numclwlk1lem2  30342  nrt2irr  30445  dipcl  30684  dipcn  30692  bcm1n  32769  expgt0b  32791  nexple  32819  2exple2exp  32820  oexpled  32822  wrdpmtrlast  33054  psgnfzto1st  33066  isarchi2  33146  submarchi  33147  znfermltl  33323  fldextrspundgdvdslem  33685  fldextrspundgdvds  33686  fldext2rspun  33687  constrext2chnlem  33755  cos9thpiminplylem2  33788  submateqlem1  33812  madjusmdetlem2  33833  madjusmdetlem4  33835  mdetlap  33837  oddpwdc  34359  eulerpartlemsv2  34363  eulerpartlemsf  34364  eulerpartlems  34365  eulerpartlemv  34369  eulerpartlemb  34373  plymulx0  34552  signsvtn0  34575  fsum2dsub  34612  reprinfz1  34627  reprpmtf1o  34631  circlemeth  34645  circlemethnat  34646  hgt750lemb  34661  hgt750lema  34662  hgt750leme  34663  tgoldbachgtde  34665  tgoldbachgtda  34666  lpadleft  34688  subfacp1lem1  35215  subfacp1lem6  35221  subfaclim  35224  erdszelem8  35234  erdszelem10  35236  cvmliftlem10  35330  faclim2  35784  poimirlem7  37667  poimirlem17  37677  poimirlem18  37678  poimirlem20  37680  poimirlem21  37681  poimirlem22  37682  poimirlem25  37685  poimirlem26  37686  poimirlem27  37687  poimirlem28  37688  poimirlem32  37692  nninfnub  37791  bfplem1  37862  zndvdchrrhm  42005  lcmineqlem1  42062  lcmineqlem2  42063  lcmineqlem8  42069  lcmineqlem10  42071  lcmineqlem11  42072  lcmineqlem15  42076  lcmineqlem16  42077  lcmineqlem18  42079  lcmineqlem19  42080  lcmineqlem20  42081  lcmineqlem21  42082  lcmineqlem22  42083  3lexlogpow2ineq2  42092  dvrelogpow2b  42101  aks4d1p1p2  42103  aks4d1p1p4  42104  aks4d1p1  42109  aks4d1p3  42111  aks4d1p7d1  42115  aks4d1p7  42116  aks4d1p8  42120  aks4d1p9  42121  isprimroot2  42127  primrootsunit1  42130  primrootscoprmpow  42132  posbezout  42133  primrootscoprbij  42135  primrootlekpowne0  42138  primrootspoweq0  42139  aks6d1c1p2  42142  aks6d1c1p3  42143  aks6d1c1p4  42144  aks6d1c1p5  42145  aks6d1c1p7  42146  aks6d1c1p6  42147  aks6d1c1p8  42148  aks6d1c2p2  42152  hashscontpowcl  42153  hashscontpow1  42154  hashscontpow  42155  aks6d1c4  42157  aks6d1c2lem3  42159  aks6d1c2lem4  42160  aks6d1c2  42163  sticksstones6  42184  sticksstones7  42185  sticksstones10  42188  sticksstones12a  42190  sticksstones12  42191  sticksstones20  42199  sticksstones22  42201  aks6d1c6lem2  42204  aks6d1c6lem3  42205  aks6d1c6lem4  42206  aks6d1c6isolem1  42207  aks6d1c6isolem2  42208  aks6d1c6lem5  42210  bcled  42211  bcle2d  42212  aks6d1c7lem1  42213  aks6d1c7  42217  aks5lem2  42220  aks5lem3a  42222  aks5lem5a  42224  grpods  42227  unitscyglem2  42229  unitscyglem4  42231  aks5lem7  42233  aks5  42237  sumcubes  42346  oexpreposd  42355  exp11d  42359  dvdsexpb  42368  fiabv  42569  fsuppind  42623  dffltz  42667  fltdvdsabdvdsc  42671  fltne  42677  flt4lem4  42682  flt4lem7  42692  fltltc  42694  fltnltalem  42695  fltnlta  42696  3rexfrabdioph  42830  4rexfrabdioph  42831  6rexfrabdioph  42832  7rexfrabdioph  42833  irrapxlem5  42859  pellexlem2  42863  pellexlem6  42867  pell14qrgt0  42892  pell1qrge1  42903  pellfundgt1  42916  ltrmxnn0  42982  jm2.26lem3  43034  jm2.27a  43038  jm2.27c  43040  rmxdiophlem  43048  jm3.1lem1  43050  jm3.1lem2  43051  jm3.1lem3  43052  jm3.1  43053  dgrsub2  43168  mpaaeu  43183  idomsubgmo  43226  relexpxpmin  43750  nzprmdif  44352  binomcxplemwb  44381  fperiodmul  45345  xralrple4  45411  fsumnncl  45612  dvsinexp  45949  dvxpaek  45978  itgsinexplem1  45992  stoweidlem1  46039  stoweidlem17  46055  stoweidlem25  46063  stoweidlem34  46072  stoweidlem38  46076  stoweidlem40  46078  stoweidlem42  46080  stoweidlem45  46083  stirlinglem4  46115  stirlinglem5  46116  stirlinglem10  46121  stirlinglem13  46124  dirkertrigeq  46139  fourierdlem21  46166  fourierdlem25  46170  fourierdlem48  46192  fourierdlem54  46198  fourierdlem64  46208  fourierdlem65  46209  fourierdlem73  46217  fourierdlem81  46225  fourierdlem83  46227  fourierdlem92  46236  fourierdlem103  46247  fourierdlem104  46248  fourierdlem112  46256  fourierdlem113  46257  etransclem1  46273  etransclem4  46276  etransclem8  46280  etransclem15  46287  etransclem17  46289  etransclem18  46290  etransclem19  46291  etransclem20  46292  etransclem21  46293  etransclem22  46294  etransclem23  46295  etransclem24  46296  etransclem25  46297  etransclem27  46299  etransclem32  46304  etransclem35  46307  etransclem41  46313  etransclem44  46316  etransclem46  46318  modmknepk  47393  iccpartigtl  47454  iccpartgt  47458  iccpartgel  47460  iccelpart  47464  odz2prm2pw  47594  fmtnoprmfac1  47596  fmtnoprmfac2  47598  2pwp1prm  47620  sfprmdvdsmersenne  47634  lighneallem4a  47639  proththdlem  47644  proththd  47645  perfectALTVlem1  47752  perfectALTVlem2  47753  perfectALTV  47754  fpprwpprb  47771  gpgedgvtx1  48093  logbpw2m1  48599  nnpw2blenfzo  48613  nnolog2flm1  48622  dignn0fr  48633  nn0sumshdiglemA  48651  nn0sumshdiglemB  48652