Theorem nnnn0 12529

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℕcn 12251  ℕ₀cn0 12522

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925  df-n0 12523

This theorem is used by:  nnnn0i  12530  elnnnn0b  12566  elnnnn0c  12567  elz2  12627  nn0ind-raph  12714  zindd  12715  fzo1fzo0n0  13763  ubmelfzo  13778  elfzom1elp1fzo  13780  fzo0sn0fzo1  13803  quoremnn0ALT  13910  modmulnn  13942  modsumfzodifsn  14000  addmodlteq  14002  expneg  14125  expcllem  14128  expcl2lem  14129  expeq0  14148  mulexpz  14158  expmordi  14223  rpexpmord  14224  expnlbnd  14289  expmulnbnd  14291  digit2  14292  digit1  14293  facmapnn  14341  facdiv  14343  faclbnd  14346  faclbnd3  14348  faclbnd4lem3  14351  faclbnd4lem4  14352  faclbnd5  14354  faclbnd6  14355  bcval5  14374  ishashinf  14520  iswrdi  14574  pfxn0  14748  repswfsts  14844  repswlsw  14845  repswcshw  14875  relexpnnrn  15108  relexpaddg  15116  absexpz  15382  isercoll  15745  summolem3  15791  summolem2a  15792  climcndslem2  15930  climcnds  15931  harmonic  15939  arisum  15940  expcnv  15944  geo2sum  15953  geo2lim  15955  geoisum1  15959  geoisum1c  15960  0.999...  15961  mertenslem2  15965  fallfacfwd  16115  0fallfac  16116  0risefac  16117  ef0lem  16157  ege2le3  16169  efaddlem  16172  efexp  16182  rpnnen2lem2  16296  rpnnen2lem4  16298  ruclem12  16322  dvdsmodexp  16343  dvdsexp2im  16410  nn0enne  16460  nnehalf  16462  nno  16465  nn0o  16466  pwp1fsum  16474  divalg2  16488  ndvdssub  16492  gcdmultiplez  16618  gcddiv  16634  rpmulgcd  16640  rplpwr  16641  nn0expgcd  16647  dvdssqlem  16649  eucalgf  16666  lcmflefac  16731  1nprm  16762  2mulprm  16776  isprm5  16791  isprm6  16798  prmdvdsexp  16799  phicl2  16852  phibndlem  16854  phiprmpw  16860  crth  16862  eulerthlem2  16866  hashgcdlem  16872  phisum  16875  pythagtriplem10  16905  pythagtriplem6  16906  pythagtriplem7  16907  pythagtriplem12  16911  pythagtriplem14  16913  pclem  16923  pcexp  16944  pcid  16958  pcprod  16980  pcbc  16985  prmpwdvds  16989  infpnlem1  16995  infpnlem2  16996  prmunb  16999  prmreclem6  17006  1arith  17012  vdwapf  17057  0hashbc  17092  ram0  17107  prmdvdsprmo  17127  prmdvdsprmop  17128  prmolefac  17131  prmgaplem1  17134  prmgaplem2  17135  prmgapprmolem  17146  prmgapprmo  17147  cshwrepswhash1  17187  smndex1n0mnd  19005  ghmmulg  19329  odmodnn0  19641  dfod2  19665  submod  19670  prmirredlem  21659  prmirred  21661  znf1o  21738  znhash  21745  znfi  21746  znfld  21747  znidomb  21748  znunithash  21751  znrrg  21752  frobrhm  21762  cply1mul  22493  cply1coe0  22498  cply1coe0bi  22499  ply1fermltlchr  22509  cpmatmcllem  22912  m2cpm  22935  m2cpminvid2lem  22948  fvmptnn04ifa  23044  chfacfisf  23048  chfacfisfcpmat  23049  chfacffsupp  23050  chfacfscmul0  23052  chfacfscmulfsupp  23053  chfacfscmulgsum  23054  chfacfpmmul0  23056  chfacfpmmulfsupp  23057  chfacfpmmulgsum  23058  chfacfpmmulgsum2  23059  cayhamlem1  23060  cpmadugsumlemF  23070  tgpmulg  24287  cmodscexp  25317  cphipval  25439  ovollb2lem  25684  ovoliunlem1  25698  ovoliunlem3  25700  uniioombllem3  25781  uniioombllem4  25782  opnmbllem  25797  mbfi1fseqlem1  25911  mbfi1fseqlem3  25913  mbfi1fseqlem4  25914  mbfi1fseqlem5  25915  mbfi1fseqlem6  25916  dvexp  26149  dvexp3  26174  idomrootle  26367  plyco  26435  dgrcolem1  26467  plydivex  26495  aaliou3lem2  26543  aaliou3lem3  26544  aaliou3lem5  26547  aaliou3lem6  26548  aaliou3lem7  26549  aaliou3lem9  26550  radcnvlem2  26614  dvradcnv  26621  pserdv2  26630  abelthlem6  26636  abelthlem9  26640  logtayllem  26861  logtayl  26862  logtaylsum  26863  logtayl2  26864  cxproot  26892  root1id  26956  logbgcd1irr  26996  atantayl  27139  atantayl2  27140  leibpilem2  27143  leibpi  27144  birthdaylem2  27154  birthdaylem3  27155  dfef2  27172  basellem2  27283  basellem4  27285  basellem5  27286  basellem6  27287  basellem8  27289  isppw2  27316  vmappw  27317  sqf11  27340  vma1  27367  1sgm2ppw  27401  chtublem  27412  fsumvma2  27415  vmasum  27417  dchrelbas4  27444  dchrzrhcl  27446  dchrfi  27456  dchrhash  27472  pcbcctr  27477  bclbnd  27481  bposlem1  27485  lgsval4a  27520  lgsdchrval  27555  lgsdchr  27556  gausslemma2dlem0c  27559  gausslemma2dlem0d  27560  gausslemma2dlem6  27573  2lgslem1a1  27590  2lgslem1c  27594  2lgslem3a1  27601  2lgslem3b1  27602  2lgslem3c1  27603  2lgslem3d1  27604  2sqreunnlem1  27650  2sqreunnltblem  27652  rplogsumlem2  27686  dchrisumlem2  27691  ostth2lem1  27819  ostth2lem3  27836  ostth3  27839  cusgrsize2inds  29840  pthdivtx  30113  cyclnumvtx  30186  crctcshwlkn0lem4  30199  crctcshwlkn0lem5  30200  crctcshwlkn0lem7  30202  0enwwlksnge1  30250  rusgr0edg  30362  clwlkclwwlkf1lem2  30393  clwlkclwwlkf1lem3  30394  clwwisshclwwslem  30402  clwwlkinwwlk  30428  clwwlkel  30434  clwwlkf  30435  clwwlkf1  30437  clwwlknwwlksnb  30443  wwlksubclwwlk  30446  erclwwlknref  30457  clwwlknonwwlknonb  30494  numclwwlkqhash  30763  numclwwlk2lem1  30764  numclwlk2lem2f  30765  numclwlk2lem2f1o  30767  ipval2  31096  ipasslem3  31222  ipasslem4  31223  nn0min  33202  znfermltl  33712  ply1fermltl  33907  esumcst  34484  eulerpartlemb  34790  fibp1  34823  ballotlem1  34909  subfacp1lem6  35698  subfaclim  35701  subfacval3  35702  snmlff  35842  bcprod  36251  faclim2  36261  nn0prpwlem  36874  knoppndvlem18  37159  opnmbllem0  38348  nnubfi  38442  nninfnub  38443  geomcau  38451  heiborlem5  38507  heiborlem6  38508  heiborlem7  38509  heiborlem8  38510  bfplem1  38514  lcmineqlem12  42848  aks4d1p1p2  42878  primrootscoprmpow  42907  2ap1caineq  42953  dvdsexpnn  43135  dvdsexpnn0  43136  zaddcomlem  43278  fidomncyc  43344  dffltz  43407  fltnltalem  43435  irrapxlem2  43591  pellexlem1  43597  pellexlem5  43601  pellqrex  43647  monotoddzzfi  43710  jm2.17c  43730  acongeq  43751  jm2.18  43756  jm2.23  43764  jm2.26lem3  43769  jm3.1  43788  expdiophlem1  43789  idomodle  43959  proot1ex  43964  rp-isfinite6  44285  cnvtrclfv  44491  cotrclrcl  44509  inductionexd  44922  binomcxplemnotnn0  45107  nnne1ge2  46051  dvnmptconst  46696  stoweidlem3  46758  stoweidlem7  46762  stoweidlem34  46789  wallispilem4  46823  wallispilem5  46824  wallispi2lem1  46826  wallispi2lem2  46827  stirlinglem2  46830  stirlinglem3  46831  stirlinglem4  46832  stirlinglem5  46833  stirlinglem7  46835  stirlinglem11  46839  stirlinglem14  46842  stirlinglem15  46843  stirlingr  46845  fourierdlem15  46877  fourierdlem21  46883  fourierdlem22  46884  fourierdlem92  46953  fourierdlem112  46973  fouriersw  46986  sge0rpcpnf  47176  sge0ad2en  47186  ovnsubaddlem1  47325  ovnsubaddlem2  47326  ovolval5lem1  47407  ovolval5lem2  47408  ceilhalfelfzo1  48112  modlt0b  48147  muldvdsfacm1  48165  iccpartiltu  48212  iccpartigtl  48213  iccpartlt  48214  iccpartleu  48218  iccpartrn  48220  iccelpart  48223  iccpartiun  48224  iccpartdisj  48227  sqrtpwpw2p  48331  fmtnosqrt  48332  odz2prm2pw  48356  fmtnoprmfac1lem  48357  fmtnoprmfac1  48358  2pwp1prm  48382  lighneallem1  48398  lighneallem2  48399  lighneallem3  48400  lighneallem4a  48401  lighneallem4  48403  nnpw2evenALTV  48508  dfwppr  48544  gpgorder  48865  gpgedgvtx0  48867  gpgedgvtx1  48868  cznabel  49066  cznrng  49067  ztprmneprm  49168  altgsumbc  49173  altgsumbcALT  49174  pw2m1lepw2m1  49341  nneom  49348  logbpw2m1  49388  blennn  49396  blenpw2m1  49400  blengt1fldiv2p1  49414  dignn0ldlem  49423  dignnld  49424  dig2nn1st  49426  dignn0flhalflem1  49436  nn0sumshdiglemA  49440  nn0sumshdiglemB  49441  itcovalt2lem2lem1  49494  eenglngeehlnm  49560