Theorem nnnn0 12409

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 12405	. 2 ⊢ ℕ ⊆ ℕ0
2	1	sseli 3933	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2109  ℕcn 12146  ℕ₀cn0 12402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-ss 3922  df-n0 12403

This theorem is referenced by:  nnnn0i  12410  elnnnn0b  12446  elnnnn0c  12447  elz2  12507  nn0ind-raph  12594  zindd  12595  fzo1fzo0n0  13636  ubmelfzo  13651  elfzom1elp1fzo  13653  fzo0sn0fzo1  13676  quoremnn0ALT  13779  modmulnn  13811  modsumfzodifsn  13869  addmodlteq  13871  expneg  13994  expcllem  13997  expcl2lem  13998  expeq0  14017  mulexpz  14027  expmordi  14092  rpexpmord  14093  expnlbnd  14158  expmulnbnd  14160  digit2  14161  digit1  14162  facmapnn  14210  facdiv  14212  faclbnd  14215  faclbnd3  14217  faclbnd4lem3  14220  faclbnd4lem4  14221  faclbnd5  14223  faclbnd6  14224  bcval5  14243  ishashinf  14388  iswrdi  14442  pfxn0  14611  repswfsts  14705  repswlsw  14706  repswcshw  14736  relexpnnrn  14970  relexpaddg  14978  absexpz  15230  isercoll  15593  summolem3  15639  summolem2a  15640  climcndslem2  15775  climcnds  15776  harmonic  15784  arisum  15785  expcnv  15789  geo2sum  15798  geo2lim  15800  geoisum1  15804  geoisum1c  15805  0.999...  15806  mertenslem2  15810  fallfacfwd  15961  0fallfac  15962  0risefac  15963  ef0lem  16003  ege2le3  16015  efaddlem  16018  efexp  16028  rpnnen2lem2  16142  rpnnen2lem4  16144  ruclem12  16168  dvdsmodexp  16189  dvdsexp2im  16256  nn0enne  16306  nnehalf  16308  nno  16311  nn0o  16312  pwp1fsum  16320  divalg2  16334  ndvdssub  16338  gcdmultiplez  16464  gcddiv  16480  rpmulgcd  16486  rplpwr  16487  nn0expgcd  16493  dvdssqlem  16495  eucalgf  16512  lcmflefac  16577  1nprm  16608  2mulprm  16622  isprm5  16636  isprm6  16643  prmdvdsexp  16644  phicl2  16697  phibndlem  16699  phiprmpw  16705  crth  16707  eulerthlem2  16711  hashgcdlem  16717  phisum  16720  pythagtriplem10  16750  pythagtriplem6  16751  pythagtriplem7  16752  pythagtriplem12  16756  pythagtriplem14  16758  pclem  16768  pcexp  16789  pcid  16803  pcprod  16825  pcbc  16830  prmpwdvds  16834  infpnlem1  16840  infpnlem2  16841  prmunb  16844  prmreclem6  16851  1arith  16857  vdwapf  16902  0hashbc  16937  ram0  16952  prmdvdsprmo  16972  prmdvdsprmop  16973  prmolefac  16976  prmgaplem1  16979  prmgaplem2  16980  prmgapprmolem  16991  prmgapprmo  16992  cshwrepswhash1  17032  smndex1n0mnd  18804  ghmmulg  19125  odmodnn0  19437  dfod2  19461  submod  19466  prmirredlem  21397  prmirred  21399  znf1o  21476  znhash  21483  znfi  21484  znfld  21485  znidomb  21486  znunithash  21489  znrrg  21490  frobrhm  21500  cply1mul  22199  cply1coe0  22204  cply1coe0bi  22205  ply1fermltlchr  22215  cpmatmcllem  22621  m2cpm  22644  m2cpminvid2lem  22657  fvmptnn04ifa  22753  chfacfisf  22757  chfacfisfcpmat  22758  chfacffsupp  22759  chfacfscmul0  22761  chfacfscmulfsupp  22762  chfacfscmulgsum  22763  chfacfpmmul0  22765  chfacfpmmulfsupp  22766  chfacfpmmulgsum  22767  chfacfpmmulgsum2  22768  cayhamlem1  22769  cpmadugsumlemF  22779  tgpmulg  23996  cmodscexp  25037  cphipval  25159  ovollb2lem  25405  ovoliunlem1  25419  ovoliunlem3  25421  uniioombllem3  25502  uniioombllem4  25503  opnmbllem  25518  mbfi1fseqlem1  25632  mbfi1fseqlem3  25634  mbfi1fseqlem4  25635  mbfi1fseqlem5  25636  mbfi1fseqlem6  25637  dvexp  25873  dvexp3  25898  idomrootle  26094  plyco  26162  dgrcolem1  26195  plydivex  26221  aaliou3lem2  26267  aaliou3lem3  26268  aaliou3lem5  26271  aaliou3lem6  26272  aaliou3lem7  26273  aaliou3lem9  26274  radcnvlem2  26339  dvradcnv  26346  pserdv2  26356  abelthlem6  26362  abelthlem9  26366  logtayllem  26584  logtayl  26585  logtaylsum  26586  logtayl2  26587  cxproot  26615  root1id  26680  logbgcd1irr  26720  atantayl  26863  atantayl2  26864  leibpilem2  26867  leibpi  26868  birthdaylem2  26878  birthdaylem3  26879  dfef2  26897  basellem2  27008  basellem4  27010  basellem5  27011  basellem6  27012  basellem8  27014  isppw2  27041  vmappw  27042  sqf11  27065  vma1  27092  1sgm2ppw  27127  chtublem  27138  fsumvma2  27141  vmasum  27143  dchrelbas4  27170  dchrzrhcl  27172  dchrfi  27182  dchrhash  27198  pcbcctr  27203  bclbnd  27207  bposlem1  27211  lgsval4a  27246  lgsdchrval  27281  lgsdchr  27282  gausslemma2dlem0c  27285  gausslemma2dlem0d  27286  gausslemma2dlem6  27299  2lgslem1a1  27316  2lgslem1c  27320  2lgslem3a1  27327  2lgslem3b1  27328  2lgslem3c1  27329  2lgslem3d1  27330  2sqreunnlem1  27376  2sqreunnltblem  27378  rplogsumlem2  27412  dchrisumlem2  27417  ostth2lem1  27545  ostth2lem3  27562  ostth3  27565  cusgrsize2inds  29417  pthdivtx  29690  cyclnumvtx  29763  crctcshwlkn0lem4  29776  crctcshwlkn0lem5  29777  crctcshwlkn0lem7  29779  0enwwlksnge1  29827  rusgr0edg  29936  clwlkclwwlkf1lem2  29967  clwlkclwwlkf1lem3  29968  clwwisshclwwslem  29976  clwwlkinwwlk  30002  clwwlkel  30008  clwwlkf  30009  clwwlkf1  30011  clwwlknwwlksnb  30017  wwlksubclwwlk  30020  erclwwlknref  30031  clwwlknonwwlknonb  30068  numclwwlkqhash  30337  numclwwlk2lem1  30338  numclwlk2lem2f  30339  numclwlk2lem2f1o  30341  ipval2  30669  ipasslem3  30795  ipasslem4  30796  nn0min  32778  znfermltl  33316  ply1fermltl  33532  esumcst  34032  eulerpartlemb  34338  fibp1  34371  ballotlem1  34457  subfacp1lem6  35160  subfaclim  35163  subfacval3  35164  snmlff  35304  bcprod  35713  faclim2  35723  nn0prpwlem  36298  knoppndvlem18  36505  opnmbllem0  37638  nnubfi  37732  nninfnub  37733  geomcau  37741  heiborlem5  37797  heiborlem6  37798  heiborlem7  37799  heiborlem8  37800  bfplem1  37804  lcmineqlem12  42016  aks4d1p1p2  42046  primrootscoprmpow  42075  2ap1caineq  42121  dvdsexpnn  42309  dvdsexpnn0  42310  zaddcomlem  42439  fidomncyc  42511  dffltz  42610  fltnltalem  42638  irrapxlem2  42799  pellexlem1  42805  pellexlem5  42809  pellqrex  42855  monotoddzzfi  42918  jm2.17c  42938  acongeq  42959  jm2.18  42964  jm2.23  42972  jm2.26lem3  42977  jm3.1  42996  expdiophlem1  42997  idomodle  43167  proot1ex  43172  rp-isfinite6  43494  cnvtrclfv  43700  cotrclrcl  43718  inductionexd  44131  binomcxplemnotnn0  44332  nnne1ge2  45276  dvnmptconst  45926  stoweidlem3  45988  stoweidlem7  45992  stoweidlem34  46019  wallispilem4  46053  wallispilem5  46054  wallispi2lem1  46056  wallispi2lem2  46057  stirlinglem2  46060  stirlinglem3  46061  stirlinglem4  46062  stirlinglem5  46063  stirlinglem7  46065  stirlinglem11  46069  stirlinglem14  46072  stirlinglem15  46073  stirlingr  46075  fourierdlem15  46107  fourierdlem21  46113  fourierdlem22  46114  fourierdlem92  46183  fourierdlem112  46203  fouriersw  46216  sge0rpcpnf  46406  sge0ad2en  46416  ovnsubaddlem1  46555  ovnsubaddlem2  46556  ovolval5lem1  46637  ovolval5lem2  46638  ceilhalfelfzo1  47318  modlt0b  47351  iccpartiltu  47410  iccpartigtl  47411  iccpartlt  47412  iccpartleu  47416  iccpartrn  47418  iccelpart  47421  iccpartiun  47422  iccpartdisj  47425  sqrtpwpw2p  47526  fmtnosqrt  47527  odz2prm2pw  47551  fmtnoprmfac1lem  47552  fmtnoprmfac1  47553  2pwp1prm  47577  lighneallem1  47593  lighneallem2  47594  lighneallem3  47595  lighneallem4a  47596  lighneallem4  47598  nnpw2evenALTV  47690  dfwppr  47726  gpgorder  48047  gpgedgvtx0  48049  gpgedgvtx1  48050  cznabel  48248  cznrng  48249  ztprmneprm  48335  altgsumbc  48340  altgsumbcALT  48341  pw2m1lepw2m1  48509  nneom  48516  logbpw2m1  48556  blennn  48564  blenpw2m1  48568  blengt1fldiv2p1  48582  dignn0ldlem  48591  dignnld  48592  dig2nn1st  48594  dignn0flhalflem1  48604  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  itcovalt2lem2lem1  48662  eenglngeehlnm  48728