Theorem nnnn0 12456

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℕcn 12193  ℕ₀cn0 12449

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-n0 12450

This theorem is referenced by:  nnnn0i  12457  elnnnn0b  12493  elnnnn0c  12494  elz2  12554  nn0ind-raph  12641  zindd  12642  fzo1fzo0n0  13683  ubmelfzo  13698  elfzom1elp1fzo  13700  fzo0sn0fzo1  13723  quoremnn0ALT  13826  modmulnn  13858  modsumfzodifsn  13916  addmodlteq  13918  expneg  14041  expcllem  14044  expcl2lem  14045  expeq0  14064  mulexpz  14074  expmordi  14139  rpexpmord  14140  expnlbnd  14205  expmulnbnd  14207  digit2  14208  digit1  14209  facmapnn  14257  facdiv  14259  faclbnd  14262  faclbnd3  14264  faclbnd4lem3  14267  faclbnd4lem4  14268  faclbnd5  14270  faclbnd6  14271  bcval5  14290  ishashinf  14435  iswrdi  14489  pfxn0  14658  repswfsts  14753  repswlsw  14754  repswcshw  14784  relexpnnrn  15018  relexpaddg  15026  absexpz  15278  isercoll  15641  summolem3  15687  summolem2a  15688  climcndslem2  15823  climcnds  15824  harmonic  15832  arisum  15833  expcnv  15837  geo2sum  15846  geo2lim  15848  geoisum1  15852  geoisum1c  15853  0.999...  15854  mertenslem2  15858  fallfacfwd  16009  0fallfac  16010  0risefac  16011  ef0lem  16051  ege2le3  16063  efaddlem  16066  efexp  16076  rpnnen2lem2  16190  rpnnen2lem4  16192  ruclem12  16216  dvdsmodexp  16237  dvdsexp2im  16304  nn0enne  16354  nnehalf  16356  nno  16359  nn0o  16360  pwp1fsum  16368  divalg2  16382  ndvdssub  16386  gcdmultiplez  16512  gcddiv  16528  rpmulgcd  16534  rplpwr  16535  nn0expgcd  16541  dvdssqlem  16543  eucalgf  16560  lcmflefac  16625  1nprm  16656  2mulprm  16670  isprm5  16684  isprm6  16691  prmdvdsexp  16692  phicl2  16745  phibndlem  16747  phiprmpw  16753  crth  16755  eulerthlem2  16759  hashgcdlem  16765  phisum  16768  pythagtriplem10  16798  pythagtriplem6  16799  pythagtriplem7  16800  pythagtriplem12  16804  pythagtriplem14  16806  pclem  16816  pcexp  16837  pcid  16851  pcprod  16873  pcbc  16878  prmpwdvds  16882  infpnlem1  16888  infpnlem2  16889  prmunb  16892  prmreclem6  16899  1arith  16905  vdwapf  16950  0hashbc  16985  ram0  17000  prmdvdsprmo  17020  prmdvdsprmop  17021  prmolefac  17024  prmgaplem1  17027  prmgaplem2  17028  prmgapprmolem  17039  prmgapprmo  17040  cshwrepswhash1  17080  smndex1n0mnd  18846  ghmmulg  19167  odmodnn0  19477  dfod2  19501  submod  19506  prmirredlem  21389  prmirred  21391  znf1o  21468  znhash  21475  znfi  21476  znfld  21477  znidomb  21478  znunithash  21481  znrrg  21482  frobrhm  21492  cply1mul  22190  cply1coe0  22195  cply1coe0bi  22196  ply1fermltlchr  22206  cpmatmcllem  22612  m2cpm  22635  m2cpminvid2lem  22648  fvmptnn04ifa  22744  chfacfisf  22748  chfacfisfcpmat  22749  chfacffsupp  22750  chfacfscmul0  22752  chfacfscmulfsupp  22753  chfacfscmulgsum  22754  chfacfpmmul0  22756  chfacfpmmulfsupp  22757  chfacfpmmulgsum  22758  chfacfpmmulgsum2  22759  cayhamlem1  22760  cpmadugsumlemF  22770  tgpmulg  23987  cmodscexp  25028  cphipval  25150  ovollb2lem  25396  ovoliunlem1  25410  ovoliunlem3  25412  uniioombllem3  25493  uniioombllem4  25494  opnmbllem  25509  mbfi1fseqlem1  25623  mbfi1fseqlem3  25625  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  mbfi1fseqlem6  25628  dvexp  25864  dvexp3  25889  idomrootle  26085  plyco  26153  dgrcolem1  26186  plydivex  26212  aaliou3lem2  26258  aaliou3lem3  26259  aaliou3lem5  26262  aaliou3lem6  26263  aaliou3lem7  26264  aaliou3lem9  26265  radcnvlem2  26330  dvradcnv  26337  pserdv2  26347  abelthlem6  26353  abelthlem9  26357  logtayllem  26575  logtayl  26576  logtaylsum  26577  logtayl2  26578  cxproot  26606  root1id  26671  logbgcd1irr  26711  atantayl  26854  atantayl2  26855  leibpilem2  26858  leibpi  26859  birthdaylem2  26869  birthdaylem3  26870  dfef2  26888  basellem2  26999  basellem4  27001  basellem5  27002  basellem6  27003  basellem8  27005  isppw2  27032  vmappw  27033  sqf11  27056  vma1  27083  1sgm2ppw  27118  chtublem  27129  fsumvma2  27132  vmasum  27134  dchrelbas4  27161  dchrzrhcl  27163  dchrfi  27173  dchrhash  27189  pcbcctr  27194  bclbnd  27198  bposlem1  27202  lgsval4a  27237  lgsdchrval  27272  lgsdchr  27273  gausslemma2dlem0c  27276  gausslemma2dlem0d  27277  gausslemma2dlem6  27290  2lgslem1a1  27307  2lgslem1c  27311  2lgslem3a1  27318  2lgslem3b1  27319  2lgslem3c1  27320  2lgslem3d1  27321  2sqreunnlem1  27367  2sqreunnltblem  27369  rplogsumlem2  27403  dchrisumlem2  27408  ostth2lem1  27536  ostth2lem3  27553  ostth3  27556  cusgrsize2inds  29388  pthdivtx  29664  cyclnumvtx  29737  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  crctcshwlkn0lem7  29753  0enwwlksnge1  29801  rusgr0edg  29910  clwlkclwwlkf1lem2  29941  clwlkclwwlkf1lem3  29942  clwwisshclwwslem  29950  clwwlkinwwlk  29976  clwwlkel  29982  clwwlkf  29983  clwwlkf1  29985  clwwlknwwlksnb  29991  wwlksubclwwlk  29994  erclwwlknref  30005  clwwlknonwwlknonb  30042  numclwwlkqhash  30311  numclwwlk2lem1  30312  numclwlk2lem2f  30313  numclwlk2lem2f1o  30315  ipval2  30643  ipasslem3  30769  ipasslem4  30770  nn0min  32752  znfermltl  33344  ply1fermltl  33560  esumcst  34060  eulerpartlemb  34366  fibp1  34399  ballotlem1  34485  subfacp1lem6  35179  subfaclim  35182  subfacval3  35183  snmlff  35323  bcprod  35732  faclim2  35742  nn0prpwlem  36317  knoppndvlem18  36524  opnmbllem0  37657  nnubfi  37751  nninfnub  37752  geomcau  37760  heiborlem5  37816  heiborlem6  37817  heiborlem7  37818  heiborlem8  37819  bfplem1  37823  lcmineqlem12  42035  aks4d1p1p2  42065  primrootscoprmpow  42094  2ap1caineq  42140  dvdsexpnn  42328  dvdsexpnn0  42329  zaddcomlem  42458  fidomncyc  42530  dffltz  42629  fltnltalem  42657  irrapxlem2  42818  pellexlem1  42824  pellexlem5  42828  pellqrex  42874  monotoddzzfi  42938  jm2.17c  42958  acongeq  42979  jm2.18  42984  jm2.23  42992  jm2.26lem3  42997  jm3.1  43016  expdiophlem1  43017  idomodle  43187  proot1ex  43192  rp-isfinite6  43514  cnvtrclfv  43720  cotrclrcl  43738  inductionexd  44151  binomcxplemnotnn0  44352  nnne1ge2  45296  dvnmptconst  45946  stoweidlem3  46008  stoweidlem7  46012  stoweidlem34  46039  wallispilem4  46073  wallispilem5  46074  wallispi2lem1  46076  wallispi2lem2  46077  stirlinglem2  46080  stirlinglem3  46081  stirlinglem4  46082  stirlinglem5  46083  stirlinglem7  46085  stirlinglem11  46089  stirlinglem14  46092  stirlinglem15  46093  stirlingr  46095  fourierdlem15  46127  fourierdlem21  46133  fourierdlem22  46134  fourierdlem92  46203  fourierdlem112  46223  fouriersw  46236  sge0rpcpnf  46426  sge0ad2en  46436  ovnsubaddlem1  46575  ovnsubaddlem2  46576  ovolval5lem1  46657  ovolval5lem2  46658  ceilhalfelfzo1  47335  modlt0b  47368  iccpartiltu  47427  iccpartigtl  47428  iccpartlt  47429  iccpartleu  47433  iccpartrn  47435  iccelpart  47438  iccpartiun  47439  iccpartdisj  47442  sqrtpwpw2p  47543  fmtnosqrt  47544  odz2prm2pw  47568  fmtnoprmfac1lem  47569  fmtnoprmfac1  47570  2pwp1prm  47594  lighneallem1  47610  lighneallem2  47611  lighneallem3  47612  lighneallem4a  47613  lighneallem4  47615  nnpw2evenALTV  47707  dfwppr  47743  gpgorder  48054  gpgedgvtx0  48056  gpgedgvtx1  48057  cznabel  48252  cznrng  48253  ztprmneprm  48339  altgsumbc  48344  altgsumbcALT  48345  pw2m1lepw2m1  48513  nneom  48520  logbpw2m1  48560  blennn  48568  blenpw2m1  48572  blengt1fldiv2p1  48586  dignn0ldlem  48595  dignnld  48596  dig2nn1st  48598  dignn0flhalflem1  48608  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613  itcovalt2lem2lem1  48666  eenglngeehlnm  48732