Theorem nnnn0 12594

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℕcn 12316  ℕ₀cn0 12587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-n0 12588

This theorem is used by:  nnnn0i  12595  elnnnn0b  12631  elnnnn0c  12632  elz2  12692  nn0ind-raph  12780  zindd  12781  fzo1fzo0n0  13830  ubmelfzo  13845  elfzom1elp1fzo  13847  fzo0sn0fzo1  13870  quoremnn0ALT  13977  modmulnn  14009  modsumfzodifsn  14067  addmodlteq  14069  expneg  14192  expcllem  14195  expcl2lem  14196  expeq0  14215  mulexpz  14225  expmordi  14290  rpexpmord  14291  expnlbnd  14357  expmulnbnd  14359  digit2  14360  digit1  14361  facmapnn  14409  facdiv  14411  faclbnd  14414  faclbnd3  14416  faclbnd4lem3  14419  faclbnd4lem4  14420  faclbnd5  14422  faclbnd6  14423  bcval5  14442  ishashinf  14588  iswrdi  14642  pfxn0  14816  repswfsts  14912  repswlsw  14913  repswcshw  14943  relexpnnrn  15178  relexpaddg  15186  absexpz  15452  isercoll  15815  summolem3  15860  summolem2a  15861  climcndslem2  15999  climcnds  16000  harmonic  16008  arisum  16009  expcnv  16013  geo2sum  16022  geo2lim  16024  geoisum1  16028  geoisum1c  16029  0.999...  16030  mertenslem2  16034  fallfacfwd  16182  0fallfac  16183  0risefac  16184  ef0lem  16224  ege2le3  16236  efaddlem  16239  efexp  16249  rpnnen2lem2  16363  rpnnen2lem4  16365  ruclem12  16389  dvdsmodexp  16410  dvdsexp2im  16477  nn0enne  16527  nnehalf  16529  nno  16532  nn0o  16533  pwp1fsum  16541  divalg2  16555  ndvdssub  16559  gcdmultiplez  16688  gcddiv  16704  rpmulgcd  16711  rplpwr  16712  nn0expgcd  16718  dvdsexpnn  16720  eucalgf  16738  lcmflefac  16803  1nprm  16834  2mulprm  16848  isprm5  16863  isprm6  16870  prmdvdsexp  16871  phicl2  16925  phibndlem  16927  phiprmpw  16933  crth  16935  eulerthlem2  16939  hashgcdlem  16945  phisum  16948  pythagtriplem10  16978  pythagtriplem6  16979  pythagtriplem7  16980  pythagtriplem12  16984  pythagtriplem14  16986  pclem  16996  pcexp  17017  pcid  17031  pcprod  17053  pcbc  17058  prmpwdvds  17062  infpnlem1  17068  infpnlem2  17069  prmunb  17072  prmreclem6  17079  1arith  17085  vdwapf  17130  0hashbc  17165  ram0  17180  prmdvdsprmo  17200  prmdvdsprmop  17201  prmolefac  17204  prmgaplem1  17207  prmgaplem2  17208  prmgapprmolem  17219  prmgapprmo  17220  cshwrepswhash1  17260  smndex1n0mnd  19091  ghmmulg  19422  odmodnn0  19734  dfod2  19758  submod  19763  prmirredlem  21758  prmirred  21760  znf1o  21837  znhash  21844  znfi  21845  znfld  21846  znidomb  21847  znunithash  21850  znrrg  21851  frobrhm  21861  cply1mul  22594  cply1coe0  22599  cply1coe0bi  22600  ply1fermltlchr  22610  cpmatmcllem  23016  m2cpm  23039  m2cpminvid2lem  23052  fvmptnn04ifa  23148  chfacfisf  23152  chfacfisfcpmat  23153  chfacffsupp  23154  chfacfscmul0  23156  chfacfscmulfsupp  23157  chfacfscmulgsum  23158  chfacfpmmul0  23160  chfacfpmmulfsupp  23161  chfacfpmmulgsum  23162  chfacfpmmulgsum2  23163  cayhamlem1  23164  cpmadugsumlemF  23174  tgpmulg  24392  cmodscexp  25422  cphipval  25544  ovollb2lem  25789  ovoliunlem1  25803  ovoliunlem3  25805  uniioombllem3  25886  uniioombllem4  25887  opnmbllem  25902  mbfi1fseqlem1  26016  mbfi1fseqlem3  26018  mbfi1fseqlem4  26019  mbfi1fseqlem5  26020  mbfi1fseqlem6  26021  dvexp  26253  dvexp3  26278  idomrootle  26471  plyco  26540  dgrcolem1  26572  plydivex  26600  aaliou3lem2  26652  aaliou3lem3  26653  aaliou3lem5  26656  aaliou3lem6  26657  aaliou3lem7  26658  aaliou3lem9  26659  radcnvlem2  26723  dvradcnv  26730  pserdv2  26739  abelthlem6  26745  abelthlem9  26749  logtayllem  26969  logtayl  26970  logtaylsum  26971  logtayl2  26972  cxproot  27000  root1id  27064  logbgcd1irr  27104  atantayl  27247  atantayl2  27248  leibpilem2  27251  leibpi  27252  birthdaylem2  27262  birthdaylem3  27263  dfef2  27280  basellem2  27391  basellem4  27393  basellem5  27394  basellem6  27395  basellem8  27397  isppw2  27424  vmappw  27425  sqf11  27448  vma1  27475  1sgm2ppw  27509  chtublem  27520  fsumvma2  27523  vmasum  27525  dchrelbas4  27552  dchrzrhcl  27554  dchrfi  27564  dchrhash  27580  pcbcctr  27585  bclbnd  27589  bposlem1  27593  lgsval4a  27628  lgsdchrval  27663  lgsdchr  27664  gausslemma2dlem0c  27667  gausslemma2dlem0d  27668  gausslemma2dlem6  27681  2lgslem1a1  27698  2lgslem1c  27702  2lgslem3a1  27709  2lgslem3b1  27710  2lgslem3c1  27711  2lgslem3d1  27712  2sqreunnlem1  27758  2sqreunnltblem  27760  rplogsumlem2  27794  dchrisumlem2  27799  ostth2lem1  27927  ostth2lem3  27944  ostth3  27947  fltoprm  27977  cusgrsize2inds  30016  pthdivtx  30294  cyclnumvtx  30370  crctcshwlkn0lem4  30384  crctcshwlkn0lem5  30385  crctcshwlkn0lem7  30387  0enwwlksnge1  30435  rusgr0edg  30547  clwlkclwwlkf1lem2  30578  clwlkclwwlkf1lem3  30579  clwwisshclwwslem  30587  clwwlkinwwlk  30613  clwwlkel  30619  clwwlkf  30620  clwwlkf1  30622  clwwlknwwlksnb  30628  wwlksubclwwlk  30631  erclwwlknref  30642  clwwlknonwwlknonb  30679  numclwwlkqhash  30958  numclwwlk2lem1  30959  numclwlk2lem2f  30960  numclwlk2lem2f1o  30962  ipval2  31291  ipasslem3  31417  ipasslem4  31418  nn0min  33394  znfermltl  33904  ply1fermltl  34100  esumcst  34677  eulerpartlemb  34983  fibp1  35016  ballotlem1  35102  subfacp1lem6  35919  subfaclim  35922  subfacval3  35923  snmlff  36063  bcprod  36472  faclim2  36482  nn0prpwlem  37080  knoppndvlem18  37365  opnmbllem0  38542  nnubfi  38652  nninfnub  38653  geomcau  38661  heiborlem5  38717  heiborlem6  38718  heiborlem7  38719  heiborlem8  38720  bfplem1  38724  lcmineqlem12  43058  aks4d1p1p2  43088  primrootscoprmpow  43117  2ap1caineq  43163  dvdsexpnn0  43354  zaddcomlem  43495  fidomncyc  43561  dffltz  43624  fltnltalem  43627  irrapxlem2  43783  pellexlem1  43789  pellexlem5  43793  pellqrex  43839  monotoddzzfi  43902  jm2.17c  43922  acongeq  43943  jm2.18  43948  jm2.23  43956  jm2.26lem3  43961  jm3.1  43980  expdiophlem1  43981  idomodle  44151  proot1ex  44156  rp-isfinite6  44477  cnvtrclfv  44683  cotrclrcl  44701  inductionexd  45114  binomcxplemnotnn0  45299  nnne1ge2  46250  dvnmptconst  46895  stoweidlem3  46957  stoweidlem7  46961  stoweidlem34  46988  wallispilem4  47022  wallispilem5  47023  wallispi2lem1  47025  wallispi2lem2  47026  stirlinglem2  47029  stirlinglem3  47030  stirlinglem4  47031  stirlinglem5  47032  stirlinglem7  47034  stirlinglem11  47038  stirlinglem14  47041  stirlinglem15  47042  stirlingr  47044  fourierdlem15  47076  fourierdlem21  47082  fourierdlem22  47083  fourierdlem92  47152  fourierdlem112  47172  fouriersw  47185  sge0rpcpnf  47375  sge0ad2en  47385  ovnsubaddlem1  47524  ovnsubaddlem2  47525  ovolval5lem1  47606  ovolval5lem2  47607  ceilhalfelfzo1  48348  modlt0b  48383  muldvdsfacm1  48401  iccpartiltu  48448  iccpartigtl  48449  iccpartlt  48450  iccpartleu  48454  iccpartrn  48456  iccelpart  48459  iccpartiun  48460  iccpartdisj  48463  sqrtpwpw2p  48567  fmtnosqrt  48568  odz2prm2pw  48592  fmtnoprmfac1lem  48593  fmtnoprmfac1  48594  2pwp1prm  48618  lighneallem1  48634  lighneallem2  48635  lighneallem3  48636  lighneallem4a  48637  lighneallem4  48639  nnpw2evenALTV  48744  dfwppr  48780  gpgorder  49101  gpgedgvtx0  49103  gpgedgvtx1  49104  cznabel  49301  cznrng  49302  ztprmneprm  49403  altgsumbc  49408  altgsumbcALT  49409  pw2m1lepw2m1  49576  nneom  49583  logbpw2m1  49623  blennn  49631  blenpw2m1  49635  blengt1fldiv2p1  49649  dignn0ldlem  49658  dignnld  49659  dig2nn1st  49661  dignn0flhalflem1  49671  nn0sumshdiglemA  49675  nn0sumshdiglemB  49676  itcovalt2lem2lem1  49729  eenglngeehlnm  49795