Theorem nnnn0 12444

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕcn 12174  ℕ₀cn0 12437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-n0 12438

This theorem is referenced by:  nnnn0i  12445  elnnnn0b  12481  elnnnn0c  12482  elz2  12542  nn0ind-raph  12629  zindd  12630  fzo1fzo0n0  13670  ubmelfzo  13685  elfzom1elp1fzo  13687  fzo0sn0fzo1  13710  quoremnn0ALT  13816  modmulnn  13848  modsumfzodifsn  13906  addmodlteq  13908  expneg  14031  expcllem  14034  expcl2lem  14035  expeq0  14054  mulexpz  14064  expmordi  14129  rpexpmord  14130  expnlbnd  14195  expmulnbnd  14197  digit2  14198  digit1  14199  facmapnn  14247  facdiv  14249  faclbnd  14252  faclbnd3  14254  faclbnd4lem3  14257  faclbnd4lem4  14258  faclbnd5  14260  faclbnd6  14261  bcval5  14280  ishashinf  14425  iswrdi  14479  pfxn0  14649  repswfsts  14743  repswlsw  14744  repswcshw  14774  relexpnnrn  15007  relexpaddg  15015  absexpz  15267  isercoll  15630  summolem3  15676  summolem2a  15677  climcndslem2  15815  climcnds  15816  harmonic  15824  arisum  15825  expcnv  15829  geo2sum  15838  geo2lim  15840  geoisum1  15844  geoisum1c  15845  0.999...  15846  mertenslem2  15850  fallfacfwd  16001  0fallfac  16002  0risefac  16003  ef0lem  16043  ege2le3  16055  efaddlem  16058  efexp  16068  rpnnen2lem2  16182  rpnnen2lem4  16184  ruclem12  16208  dvdsmodexp  16229  dvdsexp2im  16296  nn0enne  16346  nnehalf  16348  nno  16351  nn0o  16352  pwp1fsum  16360  divalg2  16374  ndvdssub  16378  gcdmultiplez  16504  gcddiv  16520  rpmulgcd  16526  rplpwr  16527  nn0expgcd  16533  dvdssqlem  16535  eucalgf  16552  lcmflefac  16617  1nprm  16648  2mulprm  16662  isprm5  16677  isprm6  16684  prmdvdsexp  16685  phicl2  16738  phibndlem  16740  phiprmpw  16746  crth  16748  eulerthlem2  16752  hashgcdlem  16758  phisum  16761  pythagtriplem10  16791  pythagtriplem6  16792  pythagtriplem7  16793  pythagtriplem12  16797  pythagtriplem14  16799  pclem  16809  pcexp  16830  pcid  16844  pcprod  16866  pcbc  16871  prmpwdvds  16875  infpnlem1  16881  infpnlem2  16882  prmunb  16885  prmreclem6  16892  1arith  16898  vdwapf  16943  0hashbc  16978  ram0  16993  prmdvdsprmo  17013  prmdvdsprmop  17014  prmolefac  17017  prmgaplem1  17020  prmgaplem2  17021  prmgapprmolem  17032  prmgapprmo  17033  cshwrepswhash1  17073  smndex1n0mnd  18883  ghmmulg  19203  odmodnn0  19515  dfod2  19539  submod  19544  prmirredlem  21452  prmirred  21454  znf1o  21531  znhash  21538  znfi  21539  znfld  21540  znidomb  21541  znunithash  21544  znrrg  21545  frobrhm  21555  cply1mul  22261  cply1coe0  22266  cply1coe0bi  22267  ply1fermltlchr  22277  cpmatmcllem  22683  m2cpm  22706  m2cpminvid2lem  22719  fvmptnn04ifa  22815  chfacfisf  22819  chfacfisfcpmat  22820  chfacffsupp  22821  chfacfscmul0  22823  chfacfscmulfsupp  22824  chfacfscmulgsum  22825  chfacfpmmul0  22827  chfacfpmmulfsupp  22828  chfacfpmmulgsum  22829  chfacfpmmulgsum2  22830  cayhamlem1  22831  cpmadugsumlemF  22841  tgpmulg  24058  cmodscexp  25088  cphipval  25210  ovollb2lem  25455  ovoliunlem1  25469  ovoliunlem3  25471  uniioombllem3  25552  uniioombllem4  25553  opnmbllem  25568  mbfi1fseqlem1  25682  mbfi1fseqlem3  25684  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  mbfi1fseqlem6  25687  dvexp  25920  dvexp3  25945  idomrootle  26138  plyco  26206  dgrcolem1  26238  plydivex  26263  aaliou3lem2  26309  aaliou3lem3  26310  aaliou3lem5  26313  aaliou3lem6  26314  aaliou3lem7  26315  aaliou3lem9  26316  radcnvlem2  26379  dvradcnv  26386  pserdv2  26395  abelthlem6  26401  abelthlem9  26405  logtayllem  26623  logtayl  26624  logtaylsum  26625  logtayl2  26626  cxproot  26654  root1id  26718  logbgcd1irr  26758  atantayl  26901  atantayl2  26902  leibpilem2  26905  leibpi  26906  birthdaylem2  26916  birthdaylem3  26917  dfef2  26934  basellem2  27045  basellem4  27047  basellem5  27048  basellem6  27049  basellem8  27051  isppw2  27078  vmappw  27079  sqf11  27102  vma1  27129  1sgm2ppw  27163  chtublem  27174  fsumvma2  27177  vmasum  27179  dchrelbas4  27206  dchrzrhcl  27208  dchrfi  27218  dchrhash  27234  pcbcctr  27239  bclbnd  27243  bposlem1  27247  lgsval4a  27282  lgsdchrval  27317  lgsdchr  27318  gausslemma2dlem0c  27321  gausslemma2dlem0d  27322  gausslemma2dlem6  27335  2lgslem1a1  27352  2lgslem1c  27356  2lgslem3a1  27363  2lgslem3b1  27364  2lgslem3c1  27365  2lgslem3d1  27366  2sqreunnlem1  27412  2sqreunnltblem  27414  rplogsumlem2  27448  dchrisumlem2  27453  ostth2lem1  27581  ostth2lem3  27598  ostth3  27601  cusgrsize2inds  29522  pthdivtx  29795  cyclnumvtx  29868  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  crctcshwlkn0lem7  29884  0enwwlksnge1  29932  rusgr0edg  30044  clwlkclwwlkf1lem2  30075  clwlkclwwlkf1lem3  30076  clwwisshclwwslem  30084  clwwlkinwwlk  30110  clwwlkel  30116  clwwlkf  30117  clwwlkf1  30119  clwwlknwwlksnb  30125  wwlksubclwwlk  30128  erclwwlknref  30139  clwwlknonwwlknonb  30176  numclwwlkqhash  30445  numclwwlk2lem1  30446  numclwlk2lem2f  30447  numclwlk2lem2f1o  30449  ipval2  30778  ipasslem3  30904  ipasslem4  30905  nn0min  32894  znfermltl  33426  ply1fermltl  33646  esumcst  34207  eulerpartlemb  34512  fibp1  34545  ballotlem1  34631  subfacp1lem6  35367  subfaclim  35370  subfacval3  35371  snmlff  35511  bcprod  35920  faclim2  35930  nn0prpwlem  36504  knoppndvlem18  36789  opnmbllem0  37977  nnubfi  38071  nninfnub  38072  geomcau  38080  heiborlem5  38136  heiborlem6  38137  heiborlem7  38138  heiborlem8  38139  bfplem1  38143  lcmineqlem12  42479  aks4d1p1p2  42509  primrootscoprmpow  42538  2ap1caineq  42584  dvdsexpnn  42765  dvdsexpnn0  42766  zaddcomlem  42908  fidomncyc  42980  dffltz  43067  fltnltalem  43095  irrapxlem2  43251  pellexlem1  43257  pellexlem5  43261  pellqrex  43307  monotoddzzfi  43370  jm2.17c  43390  acongeq  43411  jm2.18  43416  jm2.23  43424  jm2.26lem3  43429  jm3.1  43448  expdiophlem1  43449  idomodle  43619  proot1ex  43624  rp-isfinite6  43945  cnvtrclfv  44151  cotrclrcl  44169  inductionexd  44582  binomcxplemnotnn0  44783  nnne1ge2  45724  dvnmptconst  46369  stoweidlem3  46431  stoweidlem7  46435  stoweidlem34  46462  wallispilem4  46496  wallispilem5  46497  wallispi2lem1  46499  wallispi2lem2  46500  stirlinglem2  46503  stirlinglem3  46504  stirlinglem4  46505  stirlinglem5  46506  stirlinglem7  46508  stirlinglem11  46512  stirlinglem14  46515  stirlinglem15  46516  stirlingr  46518  fourierdlem15  46550  fourierdlem21  46556  fourierdlem22  46557  fourierdlem92  46626  fourierdlem112  46646  fouriersw  46659  sge0rpcpnf  46849  sge0ad2en  46859  ovnsubaddlem1  46998  ovnsubaddlem2  46999  ovolval5lem1  47080  ovolval5lem2  47081  nthrucw  47316  ceilhalfelfzo1  47782  modlt0b  47817  muldvdsfacm1  47835  iccpartiltu  47882  iccpartigtl  47883  iccpartlt  47884  iccpartleu  47888  iccpartrn  47890  iccelpart  47893  iccpartiun  47894  iccpartdisj  47897  sqrtpwpw2p  48001  fmtnosqrt  48002  odz2prm2pw  48026  fmtnoprmfac1lem  48027  fmtnoprmfac1  48028  2pwp1prm  48052  lighneallem1  48068  lighneallem2  48069  lighneallem3  48070  lighneallem4a  48071  lighneallem4  48073  nnpw2evenALTV  48178  dfwppr  48214  gpgorder  48535  gpgedgvtx0  48537  gpgedgvtx1  48538  cznabel  48736  cznrng  48737  ztprmneprm  48823  altgsumbc  48828  altgsumbcALT  48829  pw2m1lepw2m1  48996  nneom  49003  logbpw2m1  49043  blennn  49051  blenpw2m1  49055  blengt1fldiv2p1  49069  dignn0ldlem  49078  dignnld  49079  dig2nn1st  49081  dignn0flhalflem1  49091  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  itcovalt2lem2lem1  49149  eenglngeehlnm  49215