Theorem nnnn0 12530

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 12526	. 2 ⊢ ℕ ⊆ ℕ0
2	1	sseli 3990	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:  nnnn0i  12531  elnnnn0b  12567  elnnnn0c  12568  elz2  12628  nn0ind-raph  12715  zindd  12716  fzo1fzo0n0  13750  ubmelfzo  13765  elfzom1elp1fzo  13767  fzo0sn0fzo1  13790  quoremnn0ALT  13893  modmulnn  13925  modsumfzodifsn  13981  addmodlteq  13983  expneg  14106  expcllem  14109  expcl2lem  14110  expeq0  14129  mulexpz  14139  expmordi  14203  rpexpmord  14204  expnlbnd  14268  expmulnbnd  14270  digit2  14271  digit1  14272  facmapnn  14320  facdiv  14322  faclbnd  14325  faclbnd3  14327  faclbnd4lem3  14330  faclbnd4lem4  14331  faclbnd5  14333  faclbnd6  14334  bcval5  14353  ishashinf  14498  iswrdi  14552  pfxn0  14720  repswfsts  14815  repswlsw  14816  repswcshw  14846  relexpnnrn  15080  relexpaddg  15088  absexpz  15340  isercoll  15700  summolem3  15746  summolem2a  15747  climcndslem2  15882  climcnds  15883  harmonic  15891  arisum  15892  expcnv  15896  geo2sum  15905  geo2lim  15907  geoisum1  15911  geoisum1c  15912  0.999...  15913  mertenslem2  15917  fallfacfwd  16068  0fallfac  16069  0risefac  16070  ef0lem  16110  ege2le3  16122  efaddlem  16125  efexp  16133  rpnnen2lem2  16247  rpnnen2lem4  16249  ruclem12  16273  dvdsmodexp  16294  dvdsexp2im  16360  nn0enne  16410  nnehalf  16412  nno  16415  nn0o  16416  pwp1fsum  16424  divalg2  16438  ndvdssub  16442  gcdmultiplez  16568  gcddiv  16584  rpmulgcd  16590  rplpwr  16591  nn0expgcd  16597  dvdssqlem  16599  eucalgf  16616  lcmflefac  16681  1nprm  16712  2mulprm  16726  isprm5  16740  isprm6  16747  prmdvdsexp  16748  phicl2  16801  phibndlem  16803  phiprmpw  16809  crth  16811  eulerthlem2  16815  hashgcdlem  16821  phisum  16823  pythagtriplem10  16853  pythagtriplem6  16854  pythagtriplem7  16855  pythagtriplem12  16859  pythagtriplem14  16861  pclem  16871  pcexp  16892  pcid  16906  pcprod  16928  pcbc  16933  prmpwdvds  16937  infpnlem1  16943  infpnlem2  16944  prmunb  16947  prmreclem6  16954  1arith  16960  vdwapf  17005  0hashbc  17040  ram0  17055  prmdvdsprmo  17075  prmdvdsprmop  17076  prmolefac  17079  prmgaplem1  17082  prmgaplem2  17083  prmgapprmolem  17094  prmgapprmo  17095  cshwrepswhash1  17136  smndex1n0mnd  18937  ghmmulg  19258  odmodnn0  19572  dfod2  19596  submod  19601  prmirredlem  21500  prmirred  21502  znf1o  21587  znhash  21594  znfi  21595  znfld  21596  znidomb  21597  znunithash  21600  znrrg  21601  frobrhm  21611  cply1mul  22315  cply1coe0  22320  cply1coe0bi  22321  ply1fermltlchr  22331  cpmatmcllem  22739  m2cpm  22762  m2cpminvid2lem  22775  fvmptnn04ifa  22871  chfacfisf  22875  chfacfisfcpmat  22876  chfacffsupp  22877  chfacfscmul0  22879  chfacfscmulfsupp  22880  chfacfscmulgsum  22881  chfacfpmmul0  22883  chfacfpmmulfsupp  22884  chfacfpmmulgsum  22885  chfacfpmmulgsum2  22886  cayhamlem1  22887  cpmadugsumlemF  22897  tgpmulg  24116  cmodscexp  25167  cphipval  25290  ovollb2lem  25536  ovoliunlem1  25550  ovoliunlem3  25552  uniioombllem3  25633  uniioombllem4  25634  opnmbllem  25649  mbfi1fseqlem1  25764  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mbfi1fseqlem6  25769  dvexp  26005  dvexp3  26030  idomrootle  26226  plyco  26294  dgrcolem1  26327  plydivex  26353  aaliou3lem2  26399  aaliou3lem3  26400  aaliou3lem5  26403  aaliou3lem6  26404  aaliou3lem7  26405  aaliou3lem9  26406  radcnvlem2  26471  dvradcnv  26478  pserdv2  26488  abelthlem6  26494  abelthlem9  26498  logtayllem  26715  logtayl  26716  logtaylsum  26717  logtayl2  26718  cxproot  26746  root1id  26811  logbgcd1irr  26851  atantayl  26994  atantayl2  26995  leibpilem2  26998  leibpi  26999  birthdaylem2  27009  birthdaylem3  27010  dfef2  27028  basellem2  27139  basellem4  27141  basellem5  27142  basellem6  27143  basellem8  27145  isppw2  27172  vmappw  27173  sqf11  27196  vma1  27223  1sgm2ppw  27258  chtublem  27269  fsumvma2  27272  vmasum  27274  dchrelbas4  27301  dchrzrhcl  27303  dchrfi  27313  dchrhash  27329  pcbcctr  27334  bclbnd  27338  bposlem1  27342  lgsval4a  27377  lgsdchrval  27412  lgsdchr  27413  gausslemma2dlem0c  27416  gausslemma2dlem0d  27417  gausslemma2dlem6  27430  2lgslem1a1  27447  2lgslem1c  27451  2lgslem3a1  27458  2lgslem3b1  27459  2lgslem3c1  27460  2lgslem3d1  27461  2sqreunnlem1  27507  2sqreunnltblem  27509  rplogsumlem2  27543  dchrisumlem2  27548  ostth2lem1  27676  ostth2lem3  27693  ostth3  27696  cusgrsize2inds  29485  pthdivtx  29761  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  crctcshwlkn0lem7  29845  0enwwlksnge1  29893  rusgr0edg  30002  clwlkclwwlkf1lem2  30033  clwlkclwwlkf1lem3  30034  clwwisshclwwslem  30042  clwwlkinwwlk  30068  clwwlkel  30074  clwwlkf  30075  clwwlkf1  30077  clwwlknwwlksnb  30083  wwlksubclwwlk  30086  erclwwlknref  30097  clwwlknonwwlknonb  30134  numclwwlkqhash  30403  numclwwlk2lem1  30404  numclwlk2lem2f  30405  numclwlk2lem2f1o  30407  ipval2  30735  ipasslem3  30861  ipasslem4  30862  nn0min  32826  znfermltl  33373  ply1fermltl  33588  esumcst  34043  eulerpartlemb  34349  fibp1  34382  ballotlem1  34467  subfacp1lem6  35169  subfaclim  35172  subfacval3  35173  snmlff  35313  bcprod  35717  faclim2  35727  nn0prpwlem  36304  knoppndvlem18  36511  opnmbllem0  37642  nnubfi  37736  nninfnub  37737  geomcau  37745  heiborlem5  37801  heiborlem6  37802  heiborlem7  37803  heiborlem8  37804  bfplem1  37808  lcmineqlem12  42021  aks4d1p1p2  42051  primrootscoprmpow  42080  2ap1caineq  42126  dvdsexpnn  42346  dvdsexpnn0  42347  zaddcomlem  42457  fidomncyc  42521  dffltz  42620  fltnltalem  42648  irrapxlem2  42810  pellexlem1  42816  pellexlem5  42820  pellqrex  42866  monotoddzzfi  42930  jm2.17c  42950  acongeq  42971  jm2.18  42976  jm2.23  42984  jm2.26lem3  42989  jm3.1  43008  expdiophlem1  43009  idomodle  43179  proot1ex  43184  rp-isfinite6  43507  cnvtrclfv  43713  cotrclrcl  43731  inductionexd  44144  binomcxplemnotnn0  44351  nnne1ge2  45241  dvnmptconst  45896  stoweidlem3  45958  stoweidlem7  45962  stoweidlem34  45989  wallispilem4  46023  wallispilem5  46024  wallispi2lem1  46026  wallispi2lem2  46027  stirlinglem2  46030  stirlinglem3  46031  stirlinglem4  46032  stirlinglem5  46033  stirlinglem7  46035  stirlinglem11  46039  stirlinglem14  46042  stirlinglem15  46043  stirlingr  46045  fourierdlem15  46077  fourierdlem21  46083  fourierdlem22  46084  fourierdlem92  46153  fourierdlem112  46173  fouriersw  46186  sge0rpcpnf  46376  sge0ad2en  46386  ovnsubaddlem1  46525  ovnsubaddlem2  46526  ovolval5lem1  46607  ovolval5lem2  46608  iccpartiltu  47346  iccpartigtl  47347  iccpartlt  47348  iccpartleu  47352  iccpartrn  47354  iccelpart  47357  iccpartiun  47358  iccpartdisj  47361  sqrtpwpw2p  47462  fmtnosqrt  47463  odz2prm2pw  47487  fmtnoprmfac1lem  47488  fmtnoprmfac1  47489  2pwp1prm  47513  lighneallem1  47529  lighneallem2  47530  lighneallem3  47531  lighneallem4a  47532  lighneallem4  47534  nnpw2evenALTV  47626  dfwppr  47662  gpgorder  47947  ceilhalfelfzo1  47950  gpgedgvtx0  47953  gpgedgvtx1  47954  cznabel  48103  cznrng  48104  ztprmneprm  48191  altgsumbc  48196  altgsumbcALT  48197  pw2m1lepw2m1  48365  nneom  48376  logbpw2m1  48416  blennn  48424  blenpw2m1  48428  blengt1fldiv2p1  48442  dignn0ldlem  48451  dignnld  48452  dig2nn1st  48454  dignn0flhalflem1  48464  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  itcovalt2lem2lem1  48522  eenglngeehlnm  48588