Theorem nnnn0 12388

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℕcn 12125  ℕ₀cn0 12381

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-ss 3919  df-n0 12382

This theorem is referenced by:  nnnn0i  12389  elnnnn0b  12425  elnnnn0c  12426  elz2  12486  nn0ind-raph  12573  zindd  12574  fzo1fzo0n0  13615  ubmelfzo  13630  elfzom1elp1fzo  13632  fzo0sn0fzo1  13655  quoremnn0ALT  13761  modmulnn  13793  modsumfzodifsn  13851  addmodlteq  13853  expneg  13976  expcllem  13979  expcl2lem  13980  expeq0  13999  mulexpz  14009  expmordi  14074  rpexpmord  14075  expnlbnd  14140  expmulnbnd  14142  digit2  14143  digit1  14144  facmapnn  14192  facdiv  14194  faclbnd  14197  faclbnd3  14199  faclbnd4lem3  14202  faclbnd4lem4  14203  faclbnd5  14205  faclbnd6  14206  bcval5  14225  ishashinf  14370  iswrdi  14424  pfxn0  14594  repswfsts  14688  repswlsw  14689  repswcshw  14719  relexpnnrn  14952  relexpaddg  14960  absexpz  15212  isercoll  15575  summolem3  15621  summolem2a  15622  climcndslem2  15757  climcnds  15758  harmonic  15766  arisum  15767  expcnv  15771  geo2sum  15780  geo2lim  15782  geoisum1  15786  geoisum1c  15787  0.999...  15788  mertenslem2  15792  fallfacfwd  15943  0fallfac  15944  0risefac  15945  ef0lem  15985  ege2le3  15997  efaddlem  16000  efexp  16010  rpnnen2lem2  16124  rpnnen2lem4  16126  ruclem12  16150  dvdsmodexp  16171  dvdsexp2im  16238  nn0enne  16288  nnehalf  16290  nno  16293  nn0o  16294  pwp1fsum  16302  divalg2  16316  ndvdssub  16320  gcdmultiplez  16446  gcddiv  16462  rpmulgcd  16468  rplpwr  16469  nn0expgcd  16475  dvdssqlem  16477  eucalgf  16494  lcmflefac  16559  1nprm  16590  2mulprm  16604  isprm5  16618  isprm6  16625  prmdvdsexp  16626  phicl2  16679  phibndlem  16681  phiprmpw  16687  crth  16689  eulerthlem2  16693  hashgcdlem  16699  phisum  16702  pythagtriplem10  16732  pythagtriplem6  16733  pythagtriplem7  16734  pythagtriplem12  16738  pythagtriplem14  16740  pclem  16750  pcexp  16771  pcid  16785  pcprod  16807  pcbc  16812  prmpwdvds  16816  infpnlem1  16822  infpnlem2  16823  prmunb  16826  prmreclem6  16833  1arith  16839  vdwapf  16884  0hashbc  16919  ram0  16934  prmdvdsprmo  16954  prmdvdsprmop  16955  prmolefac  16958  prmgaplem1  16961  prmgaplem2  16962  prmgapprmolem  16973  prmgapprmo  16974  cshwrepswhash1  17014  smndex1n0mnd  18820  ghmmulg  19141  odmodnn0  19453  dfod2  19477  submod  19482  prmirredlem  21410  prmirred  21412  znf1o  21489  znhash  21496  znfi  21497  znfld  21498  znidomb  21499  znunithash  21502  znrrg  21503  frobrhm  21513  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  29433  pthdivtx  29706  cyclnumvtx  29779  crctcshwlkn0lem4  29792  crctcshwlkn0lem5  29793  crctcshwlkn0lem7  29795  0enwwlksnge1  29843  rusgr0edg  29952  clwlkclwwlkf1lem2  29983  clwlkclwwlkf1lem3  29984  clwwisshclwwslem  29992  clwwlkinwwlk  30018  clwwlkel  30024  clwwlkf  30025  clwwlkf1  30027  clwwlknwwlksnb  30033  wwlksubclwwlk  30036  erclwwlknref  30047  clwwlknonwwlknonb  30084  numclwwlkqhash  30353  numclwwlk2lem1  30354  numclwlk2lem2f  30355  numclwlk2lem2f1o  30357  ipval2  30685  ipasslem3  30811  ipasslem4  30812  nn0min  32801  znfermltl  33329  ply1fermltl  33546  esumcst  34074  eulerpartlemb  34379  fibp1  34412  ballotlem1  34498  subfacp1lem6  35227  subfaclim  35230  subfacval3  35231  snmlff  35371  bcprod  35780  faclim2  35790  nn0prpwlem  36362  knoppndvlem18  36569  opnmbllem0  37702  nnubfi  37796  nninfnub  37797  geomcau  37805  heiborlem5  37861  heiborlem6  37862  heiborlem7  37863  heiborlem8  37864  bfplem1  37868  lcmineqlem12  42079  aks4d1p1p2  42109  primrootscoprmpow  42138  2ap1caineq  42184  dvdsexpnn  42372  dvdsexpnn0  42373  zaddcomlem  42502  fidomncyc  42574  dffltz  42673  fltnltalem  42701  irrapxlem2  42862  pellexlem1  42868  pellexlem5  42872  pellqrex  42918  monotoddzzfi  42981  jm2.17c  43001  acongeq  43022  jm2.18  43027  jm2.23  43035  jm2.26lem3  43040  jm3.1  43059  expdiophlem1  43060  idomodle  43230  proot1ex  43235  rp-isfinite6  43557  cnvtrclfv  43763  cotrclrcl  43781  inductionexd  44194  binomcxplemnotnn0  44395  nnne1ge2  45338  dvnmptconst  45985  stoweidlem3  46047  stoweidlem7  46051  stoweidlem34  46078  wallispilem4  46112  wallispilem5  46113  wallispi2lem1  46115  wallispi2lem2  46116  stirlinglem2  46119  stirlinglem3  46120  stirlinglem4  46121  stirlinglem5  46122  stirlinglem7  46124  stirlinglem11  46128  stirlinglem14  46131  stirlinglem15  46132  stirlingr  46134  fourierdlem15  46166  fourierdlem21  46172  fourierdlem22  46173  fourierdlem92  46242  fourierdlem112  46262  fouriersw  46275  sge0rpcpnf  46465  sge0ad2en  46475  ovnsubaddlem1  46614  ovnsubaddlem2  46615  ovolval5lem1  46696  ovolval5lem2  46697  ceilhalfelfzo1  47367  modlt0b  47400  iccpartiltu  47459  iccpartigtl  47460  iccpartlt  47461  iccpartleu  47465  iccpartrn  47467  iccelpart  47470  iccpartiun  47471  iccpartdisj  47474  sqrtpwpw2p  47575  fmtnosqrt  47576  odz2prm2pw  47600  fmtnoprmfac1lem  47601  fmtnoprmfac1  47602  2pwp1prm  47626  lighneallem1  47642  lighneallem2  47643  lighneallem3  47644  lighneallem4a  47645  lighneallem4  47647  nnpw2evenALTV  47739  dfwppr  47775  gpgorder  48096  gpgedgvtx0  48098  gpgedgvtx1  48099  cznabel  48297  cznrng  48298  ztprmneprm  48384  altgsumbc  48389  altgsumbcALT  48390  pw2m1lepw2m1  48558  nneom  48565  logbpw2m1  48605  blennn  48613  blenpw2m1  48617  blengt1fldiv2p1  48631  dignn0ldlem  48640  dignnld  48641  dig2nn1st  48643  dignn0flhalflem1  48653  nn0sumshdiglemA  48657  nn0sumshdiglemB  48658  itcovalt2lem2lem1  48711  eenglngeehlnm  48777