Theorem nnnn0 12395

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℕcn 12132  ℕ₀cn0 12388

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 2115  ax-9 2123  ax-ext 2705

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915  df-n0 12389

This theorem is referenced by:  nnnn0i  12396  elnnnn0b  12432  elnnnn0c  12433  elz2  12493  nn0ind-raph  12579  zindd  12580  fzo1fzo0n0  13617  ubmelfzo  13632  elfzom1elp1fzo  13634  fzo0sn0fzo1  13657  quoremnn0ALT  13763  modmulnn  13795  modsumfzodifsn  13853  addmodlteq  13855  expneg  13978  expcllem  13981  expcl2lem  13982  expeq0  14001  mulexpz  14011  expmordi  14076  rpexpmord  14077  expnlbnd  14142  expmulnbnd  14144  digit2  14145  digit1  14146  facmapnn  14194  facdiv  14196  faclbnd  14199  faclbnd3  14201  faclbnd4lem3  14204  faclbnd4lem4  14205  faclbnd5  14207  faclbnd6  14208  bcval5  14227  ishashinf  14372  iswrdi  14426  pfxn0  14596  repswfsts  14690  repswlsw  14691  repswcshw  14721  relexpnnrn  14954  relexpaddg  14962  absexpz  15214  isercoll  15577  summolem3  15623  summolem2a  15624  climcndslem2  15759  climcnds  15760  harmonic  15768  arisum  15769  expcnv  15773  geo2sum  15782  geo2lim  15784  geoisum1  15788  geoisum1c  15789  0.999...  15790  mertenslem2  15794  fallfacfwd  15945  0fallfac  15946  0risefac  15947  ef0lem  15987  ege2le3  15999  efaddlem  16002  efexp  16012  rpnnen2lem2  16126  rpnnen2lem4  16128  ruclem12  16152  dvdsmodexp  16173  dvdsexp2im  16240  nn0enne  16290  nnehalf  16292  nno  16295  nn0o  16296  pwp1fsum  16304  divalg2  16318  ndvdssub  16322  gcdmultiplez  16448  gcddiv  16464  rpmulgcd  16470  rplpwr  16471  nn0expgcd  16477  dvdssqlem  16479  eucalgf  16496  lcmflefac  16561  1nprm  16592  2mulprm  16606  isprm5  16620  isprm6  16627  prmdvdsexp  16628  phicl2  16681  phibndlem  16683  phiprmpw  16689  crth  16691  eulerthlem2  16695  hashgcdlem  16701  phisum  16704  pythagtriplem10  16734  pythagtriplem6  16735  pythagtriplem7  16736  pythagtriplem12  16740  pythagtriplem14  16742  pclem  16752  pcexp  16773  pcid  16787  pcprod  16809  pcbc  16814  prmpwdvds  16818  infpnlem1  16824  infpnlem2  16825  prmunb  16828  prmreclem6  16835  1arith  16841  vdwapf  16886  0hashbc  16921  ram0  16936  prmdvdsprmo  16956  prmdvdsprmop  16957  prmolefac  16960  prmgaplem1  16963  prmgaplem2  16964  prmgapprmolem  16975  prmgapprmo  16976  cshwrepswhash1  17016  smndex1n0mnd  18822  ghmmulg  19142  odmodnn0  19454  dfod2  19478  submod  19483  prmirredlem  21411  prmirred  21413  znf1o  21490  znhash  21497  znfi  21498  znfld  21499  znidomb  21500  znunithash  21503  znrrg  21504  frobrhm  21514  cply1mul  22212  cply1coe0  22217  cply1coe0bi  22218  ply1fermltlchr  22228  cpmatmcllem  22634  m2cpm  22657  m2cpminvid2lem  22670  fvmptnn04ifa  22766  chfacfisf  22770  chfacfisfcpmat  22771  chfacffsupp  22772  chfacfscmul0  22774  chfacfscmulfsupp  22775  chfacfscmulgsum  22776  chfacfpmmul0  22778  chfacfpmmulfsupp  22779  chfacfpmmulgsum  22780  chfacfpmmulgsum2  22781  cayhamlem1  22782  cpmadugsumlemF  22792  tgpmulg  24009  cmodscexp  25049  cphipval  25171  ovollb2lem  25417  ovoliunlem1  25431  ovoliunlem3  25433  uniioombllem3  25514  uniioombllem4  25515  opnmbllem  25530  mbfi1fseqlem1  25644  mbfi1fseqlem3  25646  mbfi1fseqlem4  25647  mbfi1fseqlem5  25648  mbfi1fseqlem6  25649  dvexp  25885  dvexp3  25910  idomrootle  26106  plyco  26174  dgrcolem1  26207  plydivex  26233  aaliou3lem2  26279  aaliou3lem3  26280  aaliou3lem5  26283  aaliou3lem6  26284  aaliou3lem7  26285  aaliou3lem9  26286  radcnvlem2  26351  dvradcnv  26358  pserdv2  26368  abelthlem6  26374  abelthlem9  26378  logtayllem  26596  logtayl  26597  logtaylsum  26598  logtayl2  26599  cxproot  26627  root1id  26692  logbgcd1irr  26732  atantayl  26875  atantayl2  26876  leibpilem2  26879  leibpi  26880  birthdaylem2  26890  birthdaylem3  26891  dfef2  26909  basellem2  27020  basellem4  27022  basellem5  27023  basellem6  27024  basellem8  27026  isppw2  27053  vmappw  27054  sqf11  27077  vma1  27104  1sgm2ppw  27139  chtublem  27150  fsumvma2  27153  vmasum  27155  dchrelbas4  27182  dchrzrhcl  27184  dchrfi  27194  dchrhash  27210  pcbcctr  27215  bclbnd  27219  bposlem1  27223  lgsval4a  27258  lgsdchrval  27293  lgsdchr  27294  gausslemma2dlem0c  27297  gausslemma2dlem0d  27298  gausslemma2dlem6  27311  2lgslem1a1  27328  2lgslem1c  27332  2lgslem3a1  27339  2lgslem3b1  27340  2lgslem3c1  27341  2lgslem3d1  27342  2sqreunnlem1  27388  2sqreunnltblem  27390  rplogsumlem2  27424  dchrisumlem2  27429  ostth2lem1  27557  ostth2lem3  27574  ostth3  27577  cusgrsize2inds  29434  pthdivtx  29707  cyclnumvtx  29780  crctcshwlkn0lem4  29793  crctcshwlkn0lem5  29794  crctcshwlkn0lem7  29796  0enwwlksnge1  29844  rusgr0edg  29956  clwlkclwwlkf1lem2  29987  clwlkclwwlkf1lem3  29988  clwwisshclwwslem  29996  clwwlkinwwlk  30022  clwwlkel  30028  clwwlkf  30029  clwwlkf1  30031  clwwlknwwlksnb  30037  wwlksubclwwlk  30040  erclwwlknref  30051  clwwlknonwwlknonb  30088  numclwwlkqhash  30357  numclwwlk2lem1  30358  numclwlk2lem2f  30359  numclwlk2lem2f1o  30361  ipval2  30689  ipasslem3  30815  ipasslem4  30816  nn0min  32808  znfermltl  33338  ply1fermltl  33555  esumcst  34097  eulerpartlemb  34402  fibp1  34435  ballotlem1  34521  subfacp1lem6  35250  subfaclim  35253  subfacval3  35254  snmlff  35394  bcprod  35803  faclim2  35813  nn0prpwlem  36387  knoppndvlem18  36594  opnmbllem0  37717  nnubfi  37811  nninfnub  37812  geomcau  37820  heiborlem5  37876  heiborlem6  37877  heiborlem7  37878  heiborlem8  37879  bfplem1  37883  lcmineqlem12  42154  aks4d1p1p2  42184  primrootscoprmpow  42213  2ap1caineq  42259  dvdsexpnn  42452  dvdsexpnn0  42453  zaddcomlem  42582  fidomncyc  42654  dffltz  42753  fltnltalem  42781  irrapxlem2  42941  pellexlem1  42947  pellexlem5  42951  pellqrex  42997  monotoddzzfi  43060  jm2.17c  43080  acongeq  43101  jm2.18  43106  jm2.23  43114  jm2.26lem3  43119  jm3.1  43138  expdiophlem1  43139  idomodle  43309  proot1ex  43314  rp-isfinite6  43636  cnvtrclfv  43842  cotrclrcl  43860  inductionexd  44273  binomcxplemnotnn0  44474  nnne1ge2  45417  dvnmptconst  46064  stoweidlem3  46126  stoweidlem7  46130  stoweidlem34  46157  wallispilem4  46191  wallispilem5  46192  wallispi2lem1  46194  wallispi2lem2  46195  stirlinglem2  46198  stirlinglem3  46199  stirlinglem4  46200  stirlinglem5  46201  stirlinglem7  46203  stirlinglem11  46207  stirlinglem14  46210  stirlinglem15  46211  stirlingr  46213  fourierdlem15  46245  fourierdlem21  46251  fourierdlem22  46252  fourierdlem92  46321  fourierdlem112  46341  fouriersw  46354  sge0rpcpnf  46544  sge0ad2en  46554  ovnsubaddlem1  46693  ovnsubaddlem2  46694  ovolval5lem1  46775  ovolval5lem2  46776  nthrucw  47009  ceilhalfelfzo1  47455  modlt0b  47488  iccpartiltu  47547  iccpartigtl  47548  iccpartlt  47549  iccpartleu  47553  iccpartrn  47555  iccelpart  47558  iccpartiun  47559  iccpartdisj  47562  sqrtpwpw2p  47663  fmtnosqrt  47664  odz2prm2pw  47688  fmtnoprmfac1lem  47689  fmtnoprmfac1  47690  2pwp1prm  47714  lighneallem1  47730  lighneallem2  47731  lighneallem3  47732  lighneallem4a  47733  lighneallem4  47735  nnpw2evenALTV  47827  dfwppr  47863  gpgorder  48184  gpgedgvtx0  48186  gpgedgvtx1  48187  cznabel  48385  cznrng  48386  ztprmneprm  48472  altgsumbc  48477  altgsumbcALT  48478  pw2m1lepw2m1  48646  nneom  48653  logbpw2m1  48693  blennn  48701  blenpw2m1  48705  blengt1fldiv2p1  48719  dignn0ldlem  48728  dignnld  48729  dig2nn1st  48731  dignn0flhalflem1  48741  nn0sumshdiglemA  48745  nn0sumshdiglemB  48746  itcovalt2lem2lem1  48799  eenglngeehlnm  48865