Theorem nnnn0 12442

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℕcn 12172  ℕ₀cn0 12435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907  df-n0 12436

This theorem is referenced by:  nnnn0i  12443  elnnnn0b  12479  elnnnn0c  12480  elz2  12540  nn0ind-raph  12627  zindd  12628  fzo1fzo0n0  13668  ubmelfzo  13683  elfzom1elp1fzo  13685  fzo0sn0fzo1  13708  quoremnn0ALT  13814  modmulnn  13846  modsumfzodifsn  13904  addmodlteq  13906  expneg  14029  expcllem  14032  expcl2lem  14033  expeq0  14052  mulexpz  14062  expmordi  14127  rpexpmord  14128  expnlbnd  14193  expmulnbnd  14195  digit2  14196  digit1  14197  facmapnn  14245  facdiv  14247  faclbnd  14250  faclbnd3  14252  faclbnd4lem3  14255  faclbnd4lem4  14256  faclbnd5  14258  faclbnd6  14259  bcval5  14278  ishashinf  14423  iswrdi  14477  pfxn0  14647  repswfsts  14741  repswlsw  14742  repswcshw  14772  relexpnnrn  15005  relexpaddg  15013  absexpz  15265  isercoll  15628  summolem3  15674  summolem2a  15675  climcndslem2  15813  climcnds  15814  harmonic  15822  arisum  15823  expcnv  15827  geo2sum  15836  geo2lim  15838  geoisum1  15842  geoisum1c  15843  0.999...  15844  mertenslem2  15848  fallfacfwd  15999  0fallfac  16000  0risefac  16001  ef0lem  16041  ege2le3  16053  efaddlem  16056  efexp  16066  rpnnen2lem2  16180  rpnnen2lem4  16182  ruclem12  16206  dvdsmodexp  16227  dvdsexp2im  16294  nn0enne  16344  nnehalf  16346  nno  16349  nn0o  16350  pwp1fsum  16358  divalg2  16372  ndvdssub  16376  gcdmultiplez  16502  gcddiv  16518  rpmulgcd  16524  rplpwr  16525  nn0expgcd  16531  dvdssqlem  16533  eucalgf  16550  lcmflefac  16615  1nprm  16646  2mulprm  16660  isprm5  16675  isprm6  16682  prmdvdsexp  16683  phicl2  16736  phibndlem  16738  phiprmpw  16744  crth  16746  eulerthlem2  16750  hashgcdlem  16756  phisum  16759  pythagtriplem10  16789  pythagtriplem6  16790  pythagtriplem7  16791  pythagtriplem12  16795  pythagtriplem14  16797  pclem  16807  pcexp  16828  pcid  16842  pcprod  16864  pcbc  16869  prmpwdvds  16873  infpnlem1  16879  infpnlem2  16880  prmunb  16883  prmreclem6  16890  1arith  16896  vdwapf  16941  0hashbc  16976  ram0  16991  prmdvdsprmo  17011  prmdvdsprmop  17012  prmolefac  17015  prmgaplem1  17018  prmgaplem2  17019  prmgapprmolem  17030  prmgapprmo  17031  cshwrepswhash1  17071  smndex1n0mnd  18881  ghmmulg  19201  odmodnn0  19513  dfod2  19537  submod  19542  prmirredlem  21454  prmirred  21456  znf1o  21533  znhash  21540  znfi  21541  znfld  21542  znidomb  21543  znunithash  21546  znrrg  21547  frobrhm  21557  cply1mul  22289  cply1coe0  22294  cply1coe0bi  22295  ply1fermltlchr  22305  cpmatmcllem  22708  m2cpm  22731  m2cpminvid2lem  22744  fvmptnn04ifa  22840  chfacfisf  22844  chfacfisfcpmat  22845  chfacffsupp  22846  chfacfscmul0  22848  chfacfscmulfsupp  22849  chfacfscmulgsum  22850  chfacfpmmul0  22852  chfacfpmmulfsupp  22853  chfacfpmmulgsum  22854  chfacfpmmulgsum2  22855  cayhamlem1  22856  cpmadugsumlemF  22866  tgpmulg  24083  cmodscexp  25113  cphipval  25235  ovollb2lem  25480  ovoliunlem1  25494  ovoliunlem3  25496  uniioombllem3  25577  uniioombllem4  25578  opnmbllem  25593  mbfi1fseqlem1  25707  mbfi1fseqlem3  25709  mbfi1fseqlem4  25710  mbfi1fseqlem5  25711  mbfi1fseqlem6  25712  dvexp  25945  dvexp3  25970  idomrootle  26163  plyco  26231  dgrcolem1  26263  plydivex  26288  aaliou3lem2  26334  aaliou3lem3  26335  aaliou3lem5  26338  aaliou3lem6  26339  aaliou3lem7  26340  aaliou3lem9  26341  radcnvlem2  26404  dvradcnv  26411  pserdv2  26420  abelthlem6  26426  abelthlem9  26430  logtayllem  26648  logtayl  26649  logtaylsum  26650  logtayl2  26651  cxproot  26679  root1id  26743  logbgcd1irr  26783  atantayl  26926  atantayl2  26927  leibpilem2  26930  leibpi  26931  birthdaylem2  26941  birthdaylem3  26942  dfef2  26959  basellem2  27070  basellem4  27072  basellem5  27073  basellem6  27074  basellem8  27076  isppw2  27103  vmappw  27104  sqf11  27127  vma1  27154  1sgm2ppw  27188  chtublem  27199  fsumvma2  27202  vmasum  27204  dchrelbas4  27231  dchrzrhcl  27233  dchrfi  27243  dchrhash  27259  pcbcctr  27264  bclbnd  27268  bposlem1  27272  lgsval4a  27307  lgsdchrval  27342  lgsdchr  27343  gausslemma2dlem0c  27346  gausslemma2dlem0d  27347  gausslemma2dlem6  27360  2lgslem1a1  27377  2lgslem1c  27381  2lgslem3a1  27388  2lgslem3b1  27389  2lgslem3c1  27390  2lgslem3d1  27391  2sqreunnlem1  27437  2sqreunnltblem  27439  rplogsumlem2  27473  dchrisumlem2  27478  ostth2lem1  27606  ostth2lem3  27623  ostth3  27626  cusgrsize2inds  29547  pthdivtx  29820  cyclnumvtx  29893  crctcshwlkn0lem4  29906  crctcshwlkn0lem5  29907  crctcshwlkn0lem7  29909  0enwwlksnge1  29957  rusgr0edg  30069  clwlkclwwlkf1lem2  30100  clwlkclwwlkf1lem3  30101  clwwisshclwwslem  30109  clwwlkinwwlk  30135  clwwlkel  30141  clwwlkf  30142  clwwlkf1  30144  clwwlknwwlksnb  30150  wwlksubclwwlk  30153  erclwwlknref  30164  clwwlknonwwlknonb  30201  numclwwlkqhash  30470  numclwwlk2lem1  30471  numclwlk2lem2f  30472  numclwlk2lem2f1o  30474  ipval2  30803  ipasslem3  30929  ipasslem4  30930  nn0min  32920  znfermltl  33456  ply1fermltl  33676  esumcst  34254  eulerpartlemb  34559  fibp1  34592  ballotlem1  34678  subfacp1lem6  35420  subfaclim  35423  subfacval3  35424  snmlff  35564  bcprod  35973  faclim2  35983  nn0prpwlem  36557  knoppndvlem18  36842  opnmbllem0  38030  nnubfi  38124  nninfnub  38125  geomcau  38133  heiborlem5  38189  heiborlem6  38190  heiborlem7  38191  heiborlem8  38192  bfplem1  38196  lcmineqlem12  42532  aks4d1p1p2  42562  primrootscoprmpow  42591  2ap1caineq  42637  dvdsexpnn  42817  dvdsexpnn0  42818  zaddcomlem  42960  fidomncyc  43028  dffltz  43091  fltnltalem  43119  irrapxlem2  43275  pellexlem1  43281  pellexlem5  43285  pellqrex  43331  monotoddzzfi  43394  jm2.17c  43414  acongeq  43435  jm2.18  43440  jm2.23  43448  jm2.26lem3  43453  jm3.1  43472  expdiophlem1  43473  idomodle  43643  proot1ex  43648  rp-isfinite6  43969  cnvtrclfv  44175  cotrclrcl  44193  inductionexd  44606  binomcxplemnotnn0  44807  nnne1ge2  45746  dvnmptconst  46391  stoweidlem3  46453  stoweidlem7  46457  stoweidlem34  46484  wallispilem4  46518  wallispilem5  46519  wallispi2lem1  46521  wallispi2lem2  46522  stirlinglem2  46525  stirlinglem3  46526  stirlinglem4  46527  stirlinglem5  46528  stirlinglem7  46530  stirlinglem11  46534  stirlinglem14  46537  stirlinglem15  46538  stirlingr  46540  fourierdlem15  46572  fourierdlem21  46578  fourierdlem22  46579  fourierdlem92  46648  fourierdlem112  46668  fouriersw  46681  sge0rpcpnf  46871  sge0ad2en  46881  ovnsubaddlem1  47020  ovnsubaddlem2  47021  ovolval5lem1  47102  ovolval5lem2  47103  nthrucw  47338  ceilhalfelfzo1  47804  modlt0b  47839  muldvdsfacm1  47857  iccpartiltu  47904  iccpartigtl  47905  iccpartlt  47906  iccpartleu  47910  iccpartrn  47912  iccelpart  47915  iccpartiun  47916  iccpartdisj  47919  sqrtpwpw2p  48023  fmtnosqrt  48024  odz2prm2pw  48048  fmtnoprmfac1lem  48049  fmtnoprmfac1  48050  2pwp1prm  48074  lighneallem1  48090  lighneallem2  48091  lighneallem3  48092  lighneallem4a  48093  lighneallem4  48095  nnpw2evenALTV  48200  dfwppr  48236  gpgorder  48557  gpgedgvtx0  48559  gpgedgvtx1  48560  cznabel  48758  cznrng  48759  ztprmneprm  48845  altgsumbc  48850  altgsumbcALT  48851  pw2m1lepw2m1  49018  nneom  49025  logbpw2m1  49065  blennn  49073  blenpw2m1  49077  blengt1fldiv2p1  49091  dignn0ldlem  49100  dignnld  49101  dig2nn1st  49103  dignn0flhalflem1  49113  nn0sumshdiglemA  49117  nn0sumshdiglemB  49118  itcovalt2lem2lem1  49171  eenglngeehlnm  49237