Theorem nnnn0 12512

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℕcn 12234  ℕ₀cn0 12505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923  df-n0 12506

This theorem is referenced by:  nnnn0i  12513  elnnnn0b  12549  elnnnn0c  12550  elz2  12610  nn0ind-raph  12697  zindd  12698  fzo1fzo0n0  13746  ubmelfzo  13761  elfzom1elp1fzo  13763  fzo0sn0fzo1  13786  quoremnn0ALT  13892  modmulnn  13924  modsumfzodifsn  13982  addmodlteq  13984  expneg  14107  expcllem  14110  expcl2lem  14111  expeq0  14130  mulexpz  14140  expmordi  14205  rpexpmord  14206  expnlbnd  14271  expmulnbnd  14273  digit2  14274  digit1  14275  facmapnn  14323  facdiv  14325  faclbnd  14328  faclbnd3  14330  faclbnd4lem3  14333  faclbnd4lem4  14334  faclbnd5  14336  faclbnd6  14337  bcval5  14356  ishashinf  14502  iswrdi  14556  pfxn0  14726  repswfsts  14820  repswlsw  14821  repswcshw  14851  relexpnnrn  15084  relexpaddg  15092  absexpz  15358  isercoll  15721  summolem3  15767  summolem2a  15768  climcndslem2  15906  climcnds  15907  harmonic  15915  arisum  15916  expcnv  15920  geo2sum  15929  geo2lim  15931  geoisum1  15935  geoisum1c  15936  0.999...  15937  mertenslem2  15941  fallfacfwd  16091  0fallfac  16092  0risefac  16093  ef0lem  16133  ege2le3  16145  efaddlem  16148  efexp  16158  rpnnen2lem2  16272  rpnnen2lem4  16274  ruclem12  16298  dvdsmodexp  16319  dvdsexp2im  16386  nn0enne  16436  nnehalf  16438  nno  16441  nn0o  16442  pwp1fsum  16450  divalg2  16464  ndvdssub  16468  gcdmultiplez  16594  gcddiv  16610  rpmulgcd  16616  rplpwr  16617  nn0expgcd  16623  dvdssqlem  16625  eucalgf  16642  lcmflefac  16707  1nprm  16738  2mulprm  16752  isprm5  16767  isprm6  16774  prmdvdsexp  16775  phicl2  16828  phibndlem  16830  phiprmpw  16836  crth  16838  eulerthlem2  16842  hashgcdlem  16848  phisum  16851  pythagtriplem10  16881  pythagtriplem6  16882  pythagtriplem7  16883  pythagtriplem12  16887  pythagtriplem14  16889  pclem  16899  pcexp  16920  pcid  16934  pcprod  16956  pcbc  16961  prmpwdvds  16965  infpnlem1  16971  infpnlem2  16972  prmunb  16975  prmreclem6  16982  1arith  16988  vdwapf  17033  0hashbc  17068  ram0  17083  prmdvdsprmo  17103  prmdvdsprmop  17104  prmolefac  17107  prmgaplem1  17110  prmgaplem2  17111  prmgapprmolem  17122  prmgapprmo  17123  cshwrepswhash1  17163  smndex1n0mnd  18975  ghmmulg  19299  odmodnn0  19611  dfod2  19635  submod  19640  prmirredlem  21603  prmirred  21605  znf1o  21682  znhash  21689  znfi  21690  znfld  21691  znidomb  21692  znunithash  21695  znrrg  21696  frobrhm  21706  cply1mul  22437  cply1coe0  22442  cply1coe0bi  22443  ply1fermltlchr  22453  cpmatmcllem  22856  m2cpm  22879  m2cpminvid2lem  22892  fvmptnn04ifa  22988  chfacfisf  22992  chfacfisfcpmat  22993  chfacffsupp  22994  chfacfscmul0  22996  chfacfscmulfsupp  22997  chfacfscmulgsum  22998  chfacfpmmul0  23000  chfacfpmmulfsupp  23001  chfacfpmmulgsum  23002  chfacfpmmulgsum2  23003  cayhamlem1  23004  cpmadugsumlemF  23014  tgpmulg  24231  cmodscexp  25261  cphipval  25383  ovollb2lem  25628  ovoliunlem1  25642  ovoliunlem3  25644  uniioombllem3  25725  uniioombllem4  25726  opnmbllem  25741  mbfi1fseqlem1  25855  mbfi1fseqlem3  25857  mbfi1fseqlem4  25858  mbfi1fseqlem5  25859  mbfi1fseqlem6  25860  dvexp  26093  dvexp3  26118  idomrootle  26311  plyco  26379  dgrcolem1  26411  plydivex  26439  aaliou3lem2  26487  aaliou3lem3  26488  aaliou3lem5  26491  aaliou3lem6  26492  aaliou3lem7  26493  aaliou3lem9  26494  radcnvlem2  26558  dvradcnv  26565  pserdv2  26574  abelthlem6  26580  abelthlem9  26584  logtayllem  26805  logtayl  26806  logtaylsum  26807  logtayl2  26808  cxproot  26836  root1id  26900  logbgcd1irr  26940  atantayl  27083  atantayl2  27084  leibpilem2  27087  leibpi  27088  birthdaylem2  27098  birthdaylem3  27099  dfef2  27116  basellem2  27227  basellem4  27229  basellem5  27230  basellem6  27231  basellem8  27233  isppw2  27260  vmappw  27261  sqf11  27284  vma1  27311  1sgm2ppw  27345  chtublem  27356  fsumvma2  27359  vmasum  27361  dchrelbas4  27388  dchrzrhcl  27390  dchrfi  27400  dchrhash  27416  pcbcctr  27421  bclbnd  27425  bposlem1  27429  lgsval4a  27464  lgsdchrval  27499  lgsdchr  27500  gausslemma2dlem0c  27503  gausslemma2dlem0d  27504  gausslemma2dlem6  27517  2lgslem1a1  27534  2lgslem1c  27538  2lgslem3a1  27545  2lgslem3b1  27546  2lgslem3c1  27547  2lgslem3d1  27548  2sqreunnlem1  27594  2sqreunnltblem  27596  rplogsumlem2  27630  dchrisumlem2  27635  ostth2lem1  27763  ostth2lem3  27780  ostth3  27783  cusgrsize2inds  29784  pthdivtx  30057  cyclnumvtx  30130  crctcshwlkn0lem4  30143  crctcshwlkn0lem5  30144  crctcshwlkn0lem7  30146  0enwwlksnge1  30194  rusgr0edg  30306  clwlkclwwlkf1lem2  30337  clwlkclwwlkf1lem3  30338  clwwisshclwwslem  30346  clwwlkinwwlk  30372  clwwlkel  30378  clwwlkf  30379  clwwlkf1  30381  clwwlknwwlksnb  30387  wwlksubclwwlk  30390  erclwwlknref  30401  clwwlknonwwlknonb  30438  numclwwlkqhash  30707  numclwwlk2lem1  30708  numclwlk2lem2f  30709  numclwlk2lem2f1o  30711  ipval2  31040  ipasslem3  31166  ipasslem4  31167  nn0min  33146  znfermltl  33662  ply1fermltl  33857  esumcst  34434  eulerpartlemb  34739  fibp1  34772  ballotlem1  34858  subfacp1lem6  35658  subfaclim  35661  subfacval3  35662  snmlff  35802  bcprod  36211  faclim2  36221  nn0prpwlem  36814  knoppndvlem18  37099  opnmbllem0  38288  nnubfi  38382  nninfnub  38383  geomcau  38391  heiborlem5  38447  heiborlem6  38448  heiborlem7  38449  heiborlem8  38450  bfplem1  38454  lcmineqlem12  42788  aks4d1p1p2  42818  primrootscoprmpow  42847  2ap1caineq  42893  dvdsexpnn  43075  dvdsexpnn0  43076  zaddcomlem  43218  fidomncyc  43286  dffltz  43349  fltnltalem  43377  irrapxlem2  43533  pellexlem1  43539  pellexlem5  43543  pellqrex  43589  monotoddzzfi  43652  jm2.17c  43672  acongeq  43693  jm2.18  43698  jm2.23  43706  jm2.26lem3  43711  jm3.1  43730  expdiophlem1  43731  idomodle  43901  proot1ex  43906  rp-isfinite6  44227  cnvtrclfv  44433  cotrclrcl  44451  inductionexd  44864  binomcxplemnotnn0  45049  nnne1ge2  45993  dvnmptconst  46638  stoweidlem3  46700  stoweidlem7  46704  stoweidlem34  46731  wallispilem4  46765  wallispilem5  46766  wallispi2lem1  46768  wallispi2lem2  46769  stirlinglem2  46772  stirlinglem3  46773  stirlinglem4  46774  stirlinglem5  46775  stirlinglem7  46777  stirlinglem11  46781  stirlinglem14  46784  stirlinglem15  46785  stirlingr  46787  fourierdlem15  46819  fourierdlem21  46825  fourierdlem22  46826  fourierdlem92  46895  fourierdlem112  46915  fouriersw  46928  sge0rpcpnf  47118  sge0ad2en  47128  ovnsubaddlem1  47267  ovnsubaddlem2  47268  ovolval5lem1  47349  ovolval5lem2  47350  ceilhalfelfzo1  48054  modlt0b  48089  muldvdsfacm1  48107  iccpartiltu  48154  iccpartigtl  48155  iccpartlt  48156  iccpartleu  48160  iccpartrn  48162  iccelpart  48165  iccpartiun  48166  iccpartdisj  48169  sqrtpwpw2p  48273  fmtnosqrt  48274  odz2prm2pw  48298  fmtnoprmfac1lem  48299  fmtnoprmfac1  48300  2pwp1prm  48324  lighneallem1  48340  lighneallem2  48341  lighneallem3  48342  lighneallem4a  48343  lighneallem4  48345  nnpw2evenALTV  48450  dfwppr  48486  gpgorder  48807  gpgedgvtx0  48809  gpgedgvtx1  48810  cznabel  49008  cznrng  49009  ztprmneprm  49110  altgsumbc  49115  altgsumbcALT  49116  pw2m1lepw2m1  49283  nneom  49290  logbpw2m1  49330  blennn  49338  blenpw2m1  49342  blengt1fldiv2p1  49356  dignn0ldlem  49365  dignnld  49366  dig2nn1st  49368  dignn0flhalflem1  49378  nn0sumshdiglemA  49382  nn0sumshdiglemB  49383  itcovalt2lem2lem1  49436  eenglngeehlnm  49502