Theorem nnnn0 11976

Description: A positive integer is a nonnegative integer. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nnnn0	⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)

Proof of Theorem nnnn0

Step	Hyp	Ref	Expression
1		nnssnn0 11972	. 2 ⊢ ℕ ⊆ ℕ0
2	1	sseli 3871	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2113  ℕcn 11709  ℕ₀cn0 11969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-un 3846  df-in 3848  df-ss 3858  df-n0 11970

This theorem is referenced by:  nnnn0i  11977  elnnnn0b  12013  elnnnn0c  12014  elz2  12073  nn0ind-raph  12156  zindd  12157  fzo1fzo0n0  13172  ubmelfzo  13186  elfzom1elp1fzo  13188  fzo0sn0fzo1  13210  quoremnn0ALT  13309  modmulnn  13341  modsumfzodifsn  13396  addmodlteq  13398  expneg  13522  expcllem  13525  expcl2lem  13526  expeq0  13544  mulexpz  13554  expmordi  13616  rpexpmord  13617  expnlbnd  13679  expmulnbnd  13681  digit2  13682  digit1  13683  facmapnn  13730  facdiv  13732  faclbnd  13735  faclbnd3  13737  faclbnd4lem3  13740  faclbnd4lem4  13741  faclbnd5  13743  faclbnd6  13744  bcval5  13763  ishashinf  13908  iswrdi  13952  pfxn0  14130  repswfsts  14225  repswlsw  14226  repswcshw  14256  relexpnnrn  14487  relexpaddg  14495  absexpz  14748  isercoll  15110  summolem3  15157  summolem2a  15158  climcndslem2  15291  climcnds  15292  harmonic  15300  arisum  15301  expcnv  15305  geo2sum  15314  geo2lim  15316  geoisum1  15320  geoisum1c  15321  0.999...  15322  mertenslem2  15326  fallfacfwd  15475  0fallfac  15476  0risefac  15477  ef0lem  15517  ege2le3  15528  efaddlem  15531  efexp  15539  rpnnen2lem2  15653  rpnnen2lem4  15655  ruclem12  15679  dvdsmodexp  15700  dvdsexp2im  15765  nn0enne  15815  nnehalf  15817  nno  15820  nn0o  15821  pwp1fsum  15829  divalg2  15843  ndvdssub  15847  gcdmultiplez  15972  gcddiv  15988  gcdmultipleOLD  15989  gcdmultiplezOLD  15990  rpmulgcd  15995  rplpwr  15996  dvdssqlem  16000  eucalgf  16017  lcmflefac  16082  1nprm  16113  2mulprm  16127  isprm5  16141  isprm6  16148  prmdvdsexp  16149  phicl2  16198  phibndlem  16200  phiprmpw  16206  crth  16208  eulerthlem2  16212  hashgcdlem  16218  phisum  16220  pythagtriplem10  16250  pythagtriplem6  16251  pythagtriplem7  16252  pythagtriplem12  16256  pythagtriplem14  16258  pclem  16268  pcexp  16289  pcid  16302  pcprod  16324  pcbc  16329  prmpwdvds  16333  infpnlem1  16339  infpnlem2  16340  prmunb  16343  prmreclem6  16350  1arith  16356  vdwapf  16401  0hashbc  16436  ram0  16451  prmdvdsprmo  16471  prmdvdsprmop  16472  prmolefac  16475  prmgaplem1  16478  prmgaplem2  16479  prmgapprmolem  16490  prmgapprmo  16491  cshwrepswhash1  16532  smndex1n0mnd  18186  ghmmulg  18481  odmodnn0  18779  dfod2  18802  submod  18805  prmirredlem  20306  prmirred  20308  znf1o  20363  znhash  20370  znfi  20371  znfld  20372  znidomb  20373  znunithash  20376  znrrg  20377  cply1mul  21062  cply1coe0  21067  cply1coe0bi  21068  cpmatmcllem  21462  m2cpm  21485  m2cpminvid2lem  21498  fvmptnn04ifa  21594  chfacfisf  21598  chfacfisfcpmat  21599  chfacffsupp  21600  chfacfscmul0  21602  chfacfscmulfsupp  21603  chfacfscmulgsum  21604  chfacfpmmul0  21606  chfacfpmmulfsupp  21607  chfacfpmmulgsum  21608  chfacfpmmulgsum2  21609  cayhamlem1  21610  cpmadugsumlemF  21620  tgpmulg  22837  cmodscexp  23866  cphipval  23988  ovollb2lem  24233  ovoliunlem1  24247  ovoliunlem3  24249  uniioombllem3  24330  uniioombllem4  24331  opnmbllem  24346  mbfi1fseqlem1  24460  mbfi1fseqlem3  24462  mbfi1fseqlem4  24463  mbfi1fseqlem5  24464  mbfi1fseqlem6  24465  dvexp  24697  dvexp3  24722  plyco  24982  dgrcolem1  25014  plydivex  25037  aaliou3lem2  25083  aaliou3lem3  25084  aaliou3lem5  25087  aaliou3lem6  25088  aaliou3lem7  25089  aaliou3lem9  25090  radcnvlem2  25153  dvradcnv  25160  pserdv2  25169  abelthlem6  25175  abelthlem9  25179  logtayllem  25394  logtayl  25395  logtaylsum  25396  logtayl2  25397  cxproot  25425  root1id  25487  logbgcd1irr  25524  atantayl  25667  atantayl2  25668  leibpilem2  25671  leibpi  25672  birthdaylem2  25682  birthdaylem3  25683  dfef2  25700  basellem2  25811  basellem4  25813  basellem5  25814  basellem6  25815  basellem8  25817  isppw2  25844  vmappw  25845  sqf11  25868  vma1  25895  1sgm2ppw  25928  chtublem  25939  fsumvma2  25942  vmasum  25944  dchrelbas4  25971  dchrzrhcl  25973  dchrfi  25983  dchrhash  25999  pcbcctr  26004  bclbnd  26008  bposlem1  26012  lgsval4a  26047  lgsdchrval  26082  lgsdchr  26083  gausslemma2dlem0c  26086  gausslemma2dlem0d  26087  gausslemma2dlem6  26100  2lgslem1a1  26117  2lgslem1c  26121  2lgslem3a1  26128  2lgslem3b1  26129  2lgslem3c1  26130  2lgslem3d1  26131  2sqreunnlem1  26177  2sqreunnltblem  26179  rplogsumlem2  26213  dchrisumlem2  26218  ostth2lem1  26346  ostth2lem3  26363  ostth3  26366  cusgrsize2inds  27387  pthdivtx  27662  crctcshwlkn0lem4  27743  crctcshwlkn0lem5  27744  crctcshwlkn0lem7  27746  0enwwlksnge1  27794  rusgr0edg  27903  clwlkclwwlkf1lem2  27934  clwlkclwwlkf1lem3  27935  clwwisshclwwslem  27943  clwwlkinwwlk  27969  clwwlkel  27975  clwwlkf  27976  clwwlkf1  27978  clwwlknwwlksnb  27984  wwlksubclwwlk  27987  erclwwlknref  27998  clwwlknonwwlknonb  28035  numclwwlkqhash  28304  numclwwlk2lem1  28305  numclwlk2lem2f  28306  numclwlk2lem2f1o  28308  ipval2  28634  ipasslem3  28760  ipasslem4  28761  nn0min  30701  frobrhm  31054  znfermltl  31126  ply1fermltl  31234  esumcst  31593  eulerpartlemb  31897  fibp1  31930  ballotlem1  32015  subfacp1lem6  32710  subfaclim  32713  subfacval3  32714  snmlff  32854  bcprod  33267  faclim2  33277  nn0prpwlem  34141  knoppndvlem18  34339  opnmbllem0  35425  nnubfi  35520  nninfnub  35521  geomcau  35529  heiborlem5  35585  heiborlem6  35586  heiborlem7  35587  heiborlem8  35588  bfplem1  35592  lcmineqlem12  39657  aks4d1p1p2  39686  2ap1caineq  39696  nn0expgcd  39896  dvdsexpnn  39901  dvdsexpnn0  39902  dffltz  40027  fltnltalem  40055  irrapxlem2  40201  pellexlem1  40207  pellexlem5  40211  pellqrex  40257  monotoddzzfi  40320  jm2.17c  40340  acongeq  40361  jm2.18  40366  jm2.23  40374  jm2.26lem3  40379  jm3.1  40398  expdiophlem1  40399  idomrootle  40576  idomodle  40577  proot1ex  40582  rp-isfinite6  40663  cnvtrclfv  40862  cotrclrcl  40880  inductionexd  41295  binomcxplemnotnn0  41496  nnne1ge2  42352  dvnmptconst  43008  stoweidlem3  43070  stoweidlem7  43074  stoweidlem34  43101  wallispilem4  43135  wallispilem5  43136  wallispi2lem1  43138  wallispi2lem2  43139  stirlinglem2  43142  stirlinglem3  43143  stirlinglem4  43144  stirlinglem5  43145  stirlinglem7  43147  stirlinglem11  43151  stirlinglem14  43154  stirlinglem15  43155  stirlingr  43157  fourierdlem15  43189  fourierdlem21  43195  fourierdlem22  43196  fourierdlem92  43265  fourierdlem112  43285  fouriersw  43298  sge0rpcpnf  43485  sge0ad2en  43495  ovnsubaddlem1  43634  ovnsubaddlem2  43635  ovolval5lem1  43716  ovolval5lem2  43717  iccpartiltu  44392  iccpartigtl  44393  iccpartlt  44394  iccpartleu  44398  iccpartrn  44400  iccelpart  44403  iccpartiun  44404  iccpartdisj  44407  sqrtpwpw2p  44508  fmtnosqrt  44509  odz2prm2pw  44533  fmtnoprmfac1lem  44534  fmtnoprmfac1  44535  2pwp1prm  44559  lighneallem1  44575  lighneallem2  44576  lighneallem3  44577  lighneallem4a  44578  lighneallem4  44580  nnpw2evenALTV  44672  dfwppr  44708  cznabel  45030  cznrng  45031  ztprmneprm  45201  altgsumbc  45206  altgsumbcALT  45207  pw2m1lepw2m1  45379  nneom  45391  logbpw2m1  45431  blennn  45439  blenpw2m1  45443  blengt1fldiv2p1  45457  dignn0ldlem  45466  dignnld  45467  dig2nn1st  45469  dignn0flhalflem1  45479  nn0sumshdiglemA  45483  nn0sumshdiglemB  45484  itcovalt2lem2lem1  45537  eenglngeehlnm  45603