Theorem nnnn0 12533

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℕcn 12266  ℕ₀cn0 12526

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968  df-n0 12527

This theorem is referenced by:  nnnn0i  12534  elnnnn0b  12570  elnnnn0c  12571  elz2  12631  nn0ind-raph  12718  zindd  12719  fzo1fzo0n0  13754  ubmelfzo  13769  elfzom1elp1fzo  13771  fzo0sn0fzo1  13794  quoremnn0ALT  13897  modmulnn  13929  modsumfzodifsn  13985  addmodlteq  13987  expneg  14110  expcllem  14113  expcl2lem  14114  expeq0  14133  mulexpz  14143  expmordi  14207  rpexpmord  14208  expnlbnd  14272  expmulnbnd  14274  digit2  14275  digit1  14276  facmapnn  14324  facdiv  14326  faclbnd  14329  faclbnd3  14331  faclbnd4lem3  14334  faclbnd4lem4  14335  faclbnd5  14337  faclbnd6  14338  bcval5  14357  ishashinf  14502  iswrdi  14556  pfxn0  14724  repswfsts  14819  repswlsw  14820  repswcshw  14850  relexpnnrn  15084  relexpaddg  15092  absexpz  15344  isercoll  15704  summolem3  15750  summolem2a  15751  climcndslem2  15886  climcnds  15887  harmonic  15895  arisum  15896  expcnv  15900  geo2sum  15909  geo2lim  15911  geoisum1  15915  geoisum1c  15916  0.999...  15917  mertenslem2  15921  fallfacfwd  16072  0fallfac  16073  0risefac  16074  ef0lem  16114  ege2le3  16126  efaddlem  16129  efexp  16137  rpnnen2lem2  16251  rpnnen2lem4  16253  ruclem12  16277  dvdsmodexp  16298  dvdsexp2im  16364  nn0enne  16414  nnehalf  16416  nno  16419  nn0o  16420  pwp1fsum  16428  divalg2  16442  ndvdssub  16446  gcdmultiplez  16572  gcddiv  16588  rpmulgcd  16594  rplpwr  16595  nn0expgcd  16601  dvdssqlem  16603  eucalgf  16620  lcmflefac  16685  1nprm  16716  2mulprm  16730  isprm5  16744  isprm6  16751  prmdvdsexp  16752  phicl2  16805  phibndlem  16807  phiprmpw  16813  crth  16815  eulerthlem2  16819  hashgcdlem  16825  phisum  16828  pythagtriplem10  16858  pythagtriplem6  16859  pythagtriplem7  16860  pythagtriplem12  16864  pythagtriplem14  16866  pclem  16876  pcexp  16897  pcid  16911  pcprod  16933  pcbc  16938  prmpwdvds  16942  infpnlem1  16948  infpnlem2  16949  prmunb  16952  prmreclem6  16959  1arith  16965  vdwapf  17010  0hashbc  17045  ram0  17060  prmdvdsprmo  17080  prmdvdsprmop  17081  prmolefac  17084  prmgaplem1  17087  prmgaplem2  17088  prmgapprmolem  17099  prmgapprmo  17100  cshwrepswhash1  17140  smndex1n0mnd  18925  ghmmulg  19246  odmodnn0  19558  dfod2  19582  submod  19587  prmirredlem  21483  prmirred  21485  znf1o  21570  znhash  21577  znfi  21578  znfld  21579  znidomb  21580  znunithash  21583  znrrg  21584  frobrhm  21594  cply1mul  22300  cply1coe0  22305  cply1coe0bi  22306  ply1fermltlchr  22316  cpmatmcllem  22724  m2cpm  22747  m2cpminvid2lem  22760  fvmptnn04ifa  22856  chfacfisf  22860  chfacfisfcpmat  22861  chfacffsupp  22862  chfacfscmul0  22864  chfacfscmulfsupp  22865  chfacfscmulgsum  22866  chfacfpmmul0  22868  chfacfpmmulfsupp  22869  chfacfpmmulgsum  22870  chfacfpmmulgsum2  22871  cayhamlem1  22872  cpmadugsumlemF  22882  tgpmulg  24101  cmodscexp  25154  cphipval  25277  ovollb2lem  25523  ovoliunlem1  25537  ovoliunlem3  25539  uniioombllem3  25620  uniioombllem4  25621  opnmbllem  25636  mbfi1fseqlem1  25750  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  mbfi1fseqlem6  25755  dvexp  25991  dvexp3  26016  idomrootle  26212  plyco  26280  dgrcolem1  26313  plydivex  26339  aaliou3lem2  26385  aaliou3lem3  26386  aaliou3lem5  26389  aaliou3lem6  26390  aaliou3lem7  26391  aaliou3lem9  26392  radcnvlem2  26457  dvradcnv  26464  pserdv2  26474  abelthlem6  26480  abelthlem9  26484  logtayllem  26701  logtayl  26702  logtaylsum  26703  logtayl2  26704  cxproot  26732  root1id  26797  logbgcd1irr  26837  atantayl  26980  atantayl2  26981  leibpilem2  26984  leibpi  26985  birthdaylem2  26995  birthdaylem3  26996  dfef2  27014  basellem2  27125  basellem4  27127  basellem5  27128  basellem6  27129  basellem8  27131  isppw2  27158  vmappw  27159  sqf11  27182  vma1  27209  1sgm2ppw  27244  chtublem  27255  fsumvma2  27258  vmasum  27260  dchrelbas4  27287  dchrzrhcl  27289  dchrfi  27299  dchrhash  27315  pcbcctr  27320  bclbnd  27324  bposlem1  27328  lgsval4a  27363  lgsdchrval  27398  lgsdchr  27399  gausslemma2dlem0c  27402  gausslemma2dlem0d  27403  gausslemma2dlem6  27416  2lgslem1a1  27433  2lgslem1c  27437  2lgslem3a1  27444  2lgslem3b1  27445  2lgslem3c1  27446  2lgslem3d1  27447  2sqreunnlem1  27493  2sqreunnltblem  27495  rplogsumlem2  27529  dchrisumlem2  27534  ostth2lem1  27662  ostth2lem3  27679  ostth3  27682  cusgrsize2inds  29471  pthdivtx  29747  cyclnumvtx  29820  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  crctcshwlkn0lem7  29836  0enwwlksnge1  29884  rusgr0edg  29993  clwlkclwwlkf1lem2  30024  clwlkclwwlkf1lem3  30025  clwwisshclwwslem  30033  clwwlkinwwlk  30059  clwwlkel  30065  clwwlkf  30066  clwwlkf1  30068  clwwlknwwlksnb  30074  wwlksubclwwlk  30077  erclwwlknref  30088  clwwlknonwwlknonb  30125  numclwwlkqhash  30394  numclwwlk2lem1  30395  numclwlk2lem2f  30396  numclwlk2lem2f1o  30398  ipval2  30726  ipasslem3  30852  ipasslem4  30853  nn0min  32822  znfermltl  33394  ply1fermltl  33609  esumcst  34064  eulerpartlemb  34370  fibp1  34403  ballotlem1  34489  subfacp1lem6  35190  subfaclim  35193  subfacval3  35194  snmlff  35334  bcprod  35738  faclim2  35748  nn0prpwlem  36323  knoppndvlem18  36530  opnmbllem0  37663  nnubfi  37757  nninfnub  37758  geomcau  37766  heiborlem5  37822  heiborlem6  37823  heiborlem7  37824  heiborlem8  37825  bfplem1  37829  lcmineqlem12  42041  aks4d1p1p2  42071  primrootscoprmpow  42100  2ap1caineq  42146  dvdsexpnn  42368  dvdsexpnn0  42369  zaddcomlem  42481  fidomncyc  42545  dffltz  42644  fltnltalem  42672  irrapxlem2  42834  pellexlem1  42840  pellexlem5  42844  pellqrex  42890  monotoddzzfi  42954  jm2.17c  42974  acongeq  42995  jm2.18  43000  jm2.23  43008  jm2.26lem3  43013  jm3.1  43032  expdiophlem1  43033  idomodle  43203  proot1ex  43208  rp-isfinite6  43531  cnvtrclfv  43737  cotrclrcl  43755  inductionexd  44168  binomcxplemnotnn0  44375  nnne1ge2  45303  dvnmptconst  45956  stoweidlem3  46018  stoweidlem7  46022  stoweidlem34  46049  wallispilem4  46083  wallispilem5  46084  wallispi2lem1  46086  wallispi2lem2  46087  stirlinglem2  46090  stirlinglem3  46091  stirlinglem4  46092  stirlinglem5  46093  stirlinglem7  46095  stirlinglem11  46099  stirlinglem14  46102  stirlinglem15  46103  stirlingr  46105  fourierdlem15  46137  fourierdlem21  46143  fourierdlem22  46144  fourierdlem92  46213  fourierdlem112  46233  fouriersw  46246  sge0rpcpnf  46436  sge0ad2en  46446  ovnsubaddlem1  46585  ovnsubaddlem2  46586  ovolval5lem1  46667  ovolval5lem2  46668  iccpartiltu  47409  iccpartigtl  47410  iccpartlt  47411  iccpartleu  47415  iccpartrn  47417  iccelpart  47420  iccpartiun  47421  iccpartdisj  47424  sqrtpwpw2p  47525  fmtnosqrt  47526  odz2prm2pw  47550  fmtnoprmfac1lem  47551  fmtnoprmfac1  47552  2pwp1prm  47576  lighneallem1  47592  lighneallem2  47593  lighneallem3  47594  lighneallem4a  47595  lighneallem4  47597  nnpw2evenALTV  47689  dfwppr  47725  gpgorder  48013  ceilhalfelfzo1  48016  gpgedgvtx0  48019  gpgedgvtx1  48020  cznabel  48176  cznrng  48177  ztprmneprm  48263  altgsumbc  48268  altgsumbcALT  48269  pw2m1lepw2m1  48437  nneom  48448  logbpw2m1  48488  blennn  48496  blenpw2m1  48500  blengt1fldiv2p1  48514  dignn0ldlem  48523  dignnld  48524  dig2nn1st  48526  dignn0flhalflem1  48536  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  itcovalt2lem2lem1  48594  eenglngeehlnm  48660