Theorem nnnn0 11625

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

Syntax hints:   → wi 4   ∈ wcel 2166  ℕcn 11349  ℕ₀cn0 11617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2802

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-v 3415  df-un 3802  df-in 3804  df-ss 3811  df-n0 11618

This theorem is referenced by:  nnnn0i  11626  elnnnn0b  11663  elnnnn0c  11664  elz2  11720  nn0ind-raph  11804  zindd  11805  fzo1fzo0n0  12813  ubmelfzo  12827  elfzom1elp1fzo  12829  fzo0sn0fzo1  12851  quoremnn0ALT  12950  modmulnn  12982  modsumfzodifsn  13037  addmodlteq  13039  expneg  13161  expcllem  13164  expcl2lem  13165  expeq0  13183  mulexpz  13193  expnlbnd  13287  expmulnbnd  13289  digit2  13290  digit1  13291  facmapnn  13364  facdiv  13366  faclbnd  13369  faclbnd3  13371  faclbnd4lem3  13374  faclbnd4lem4  13375  faclbnd5  13377  faclbnd6  13378  bcval5  13397  ishashinf  13535  iswrdi  13577  swrdn0OLD  13716  swrdtrcfvOLD  13729  pfxn0  13764  swrdccatwrdOLD  13799  repswfsts  13896  repswlsw  13897  repswcshw  13932  relexpnnrn  14161  relexpaddg  14169  absexpz  14421  isercoll  14774  summolem3  14821  summolem2a  14822  climcndslem2  14955  climcnds  14956  harmonic  14964  arisum  14965  expcnv  14969  geo2sum  14977  geo2lim  14979  geoisum1  14983  geoisum1c  14984  0.999...  14985  mertenslem2  14989  fallfacfwd  15138  0fallfac  15139  0risefac  15140  ef0lem  15180  ege2le3  15191  efaddlem  15194  efexp  15202  rpnnen2lem2  15317  rpnnen2lem4  15319  ruclem12  15343  dvdsmodexp  15364  nn0enne  15467  nnehalf  15469  nno  15471  nn0o  15472  pwp1fsum  15487  divalg2  15501  ndvdssub  15505  gcddiv  15640  gcdmultiple  15641  gcdmultiplez  15642  rpmulgcd  15647  rplpwr  15648  dvdssqlem  15651  eucalgf  15668  lcmflefac  15733  1nprm  15763  isprm5  15789  isprm6  15796  prmdvdsexp  15797  phicl2  15843  phibndlem  15845  phiprmpw  15851  crth  15853  eulerthlem2  15857  hashgcdlem  15863  phisum  15865  pythagtriplem10  15895  pythagtriplem6  15896  pythagtriplem7  15897  pythagtriplem12  15901  pythagtriplem14  15903  pclem  15913  pcexp  15934  pcid  15947  pcprod  15969  pcbc  15974  prmpwdvds  15978  infpnlem1  15984  infpnlem2  15985  prmunb  15988  prmreclem6  15995  1arith  16001  vdwapf  16046  0hashbc  16081  ram0  16096  prmdvdsprmo  16116  prmdvdsprmop  16117  prmolefac  16120  prmgaplem1  16123  prmgaplem2  16124  prmgapprmolem  16135  prmgapprmo  16136  cshwrepswhash1  16174  ghmmulg  18022  odmodnn0  18309  dfod2  18331  submod  18334  cply1mul  20023  cply1coe0  20028  cply1coe0bi  20029  prmirredlem  20200  prmirred  20202  znf1o  20258  znhash  20265  znfi  20266  znfld  20267  znidomb  20268  znunithash  20271  znrrg  20272  cpmatmcllem  20892  m2cpm  20915  m2cpminvid2lem  20928  fvmptnn04ifa  21024  chfacfisf  21028  chfacfisfcpmat  21029  chfacffsupp  21030  chfacfscmul0  21032  chfacfscmulfsupp  21033  chfacfscmulgsum  21034  chfacfpmmul0  21036  chfacfpmmulfsupp  21037  chfacfpmmulgsum  21038  chfacfpmmulgsum2  21039  cayhamlem1  21040  cpmadugsumlemF  21050  tgpmulg  22266  cmodscexp  23289  cphipval  23410  ovollb2lem  23653  ovoliunlem1  23667  ovoliunlem3  23669  uniioombllem3  23750  uniioombllem4  23751  opnmbllem  23766  mbfi1fseqlem1  23880  mbfi1fseqlem3  23882  mbfi1fseqlem4  23883  mbfi1fseqlem5  23884  mbfi1fseqlem6  23885  dvexp  24114  dvexp3  24139  plyco  24395  dgrcolem1  24427  plydivex  24450  aaliou3lem2  24496  aaliou3lem3  24497  aaliou3lem5  24500  aaliou3lem6  24501  aaliou3lem7  24502  aaliou3lem9  24503  radcnvlem2  24566  dvradcnv  24573  pserdv2  24582  abelthlem6  24588  abelthlem9  24592  logtayllem  24803  logtayl  24804  logtaylsum  24805  logtayl2  24806  cxproot  24834  root1id  24896  logbgcd1irr  24933  atantayl  25076  atantayl2  25077  leibpilem2  25080  leibpi  25081  birthdaylem2  25091  birthdaylem3  25092  dfef2  25109  basellem2  25220  basellem4  25222  basellem5  25223  basellem6  25224  basellem8  25226  isppw2  25253  vmappw  25254  sqf11  25277  vma1  25304  1sgm2ppw  25337  chtublem  25348  fsumvma2  25351  vmasum  25353  dchrelbas4  25380  dchrzrhcl  25382  dchrfi  25392  dchrhash  25408  pcbcctr  25413  bclbnd  25417  bposlem1  25421  lgsval4a  25456  lgsdchrval  25491  lgsdchr  25492  gausslemma2dlem0c  25495  gausslemma2dlem0d  25496  gausslemma2dlem6  25509  2lgslem1a1  25526  2lgslem1c  25530  2lgslem3a1  25537  2lgslem3b1  25538  2lgslem3c1  25539  2lgslem3d1  25540  rplogsumlem2  25586  dchrisumlem2  25591  ostth2lem1  25719  ostth2lem3  25736  ostth3  25739  cusgrsize2inds  26750  pthdivtx  27030  crctcshwlkn0lem4  27111  crctcshwlkn0lem5  27112  crctcshwlkn0lem7  27114  0enwwlksnge1  27162  rusgr0edg  27301  clwlkclwwlkf1lem2  27335  clwlkclwwlkf1lem2OLD  27336  clwlkclwwlkf1lem3  27337  clwlkclwwlkf1lem3OLD  27338  clwwisshclwwslem  27351  clwwlkinwwlk  27383  clwwlkinwwlkOLD  27384  clwwlknfi  27389  clwwlkel  27390  clwwlkfOLD  27391  clwwlkf1OLD  27393  clwwlkf  27396  clwwlkf1  27398  clwwlknwwlksnb  27406  wwlksubclwwlk  27409  wwlksubclwwlkOLD  27410  erclwwlknref  27421  clwlksf1clwwlklemOLD  27443  clwwlknonelOLD  27468  clwwlknonwwlknonb  27479  clwwlknonwwlknonbOLD  27480  numclwwlkqhash  27777  numclwwlk2lem1  27778  numclwlk2lem2f  27779  numclwlk2lem2f1o  27781  numclwlk2lem2fOLD  27782  numclwlk2lem2f1oOLD  27784  numclwwlk2lem1OLD  27789  numclwlk2lem2fOLDOLD  27790  ipval2  28116  ipasslem3  28242  ipasslem4  28243  nn0min  30113  esumcst  30669  eulerpartlemb  30974  fibp1  31008  ballotlem1  31093  subfacp1lem6  31712  subfaclim  31715  subfacval3  31716  snmlff  31856  bcprod  32165  faclim2  32175  dvdspw  32177  nn0prpwlem  32854  knoppndvlem18  33051  opnmbllem0  33988  nnubfi  34087  nninfnub  34088  geomcau  34096  heiborlem5  34155  heiborlem6  34156  heiborlem7  34157  heiborlem8  34158  bfplem1  34162  dffltz  38096  irrapxlem2  38230  pellexlem1  38236  pellexlem5  38240  pellqrex  38286  monotoddzzfi  38349  expmordi  38354  rpexpmord  38355  jm2.17c  38371  acongeq  38392  jm2.18  38397  jm2.23  38405  jm2.26lem3  38410  jm3.1  38429  expdiophlem1  38430  idomrootle  38615  idomodle  38616  proot1ex  38621  rp-isfinite6  38704  cnvtrclfv  38856  cotrclrcl  38874  inductionexd  39292  binomcxplemnotnn0  39394  nnne1ge2  40302  dvnmptconst  40950  stoweidlem3  41013  stoweidlem7  41017  stoweidlem34  41044  wallispilem4  41078  wallispilem5  41079  wallispi2lem1  41081  wallispi2lem2  41082  stirlinglem2  41085  stirlinglem3  41086  stirlinglem4  41087  stirlinglem5  41088  stirlinglem7  41090  stirlinglem11  41094  stirlinglem14  41097  stirlinglem15  41098  stirlingr  41100  fourierdlem15  41132  fourierdlem21  41138  fourierdlem22  41139  fourierdlem92  41208  fourierdlem112  41228  fouriersw  41241  sge0rpcpnf  41428  sge0ad2en  41438  ovnsubaddlem1  41577  ovnsubaddlem2  41578  ovolval5lem1  41659  ovolval5lem2  41660  iccpartiltu  42245  iccpartigtl  42246  iccpartlt  42247  iccpartleu  42251  iccpartrn  42253  iccelpart  42256  iccpartiun  42257  iccpartdisj  42260  sqrtpwpw2p  42279  fmtnosqrt  42280  odz2prm2pw  42304  fmtnoprmfac1lem  42305  fmtnoprmfac1  42306  2pwp1prm  42332  lighneallem1  42351  lighneallem2  42352  lighneallem3  42353  lighneallem4a  42354  lighneallem4  42356  nnpw2evenALTV  42440  cznabel  42800  cznrng  42801  ztprmneprm  42971  altgsumbc  42976  altgsumbcALT  42977  pw2m1lepw2m1  43156  nneom  43167  logbpw2m1  43207  blennn  43215  blenpw2m1  43219  blengt1fldiv2p1  43233  dignn0ldlem  43242  dignnld  43243  dig2nn1st  43245  dignn0flhalflem1  43255  nn0sumshdiglemA  43259  nn0sumshdiglemB  43260  eenglngeehlnm  43289