Theorem nnnn0 12506

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℕcn 12238  ℕ₀cn0 12499

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943  df-n0 12500

This theorem is referenced by:  nnnn0i  12507  elnnnn0b  12543  elnnnn0c  12544  elz2  12604  nn0ind-raph  12691  zindd  12692  fzo1fzo0n0  13729  ubmelfzo  13744  elfzom1elp1fzo  13746  fzo0sn0fzo1  13769  quoremnn0ALT  13872  modmulnn  13904  modsumfzodifsn  13960  addmodlteq  13962  expneg  14085  expcllem  14088  expcl2lem  14089  expeq0  14108  mulexpz  14118  expmordi  14183  rpexpmord  14184  expnlbnd  14249  expmulnbnd  14251  digit2  14252  digit1  14253  facmapnn  14301  facdiv  14303  faclbnd  14306  faclbnd3  14308  faclbnd4lem3  14311  faclbnd4lem4  14312  faclbnd5  14314  faclbnd6  14315  bcval5  14334  ishashinf  14479  iswrdi  14533  pfxn0  14702  repswfsts  14797  repswlsw  14798  repswcshw  14828  relexpnnrn  15062  relexpaddg  15070  absexpz  15322  isercoll  15682  summolem3  15728  summolem2a  15729  climcndslem2  15864  climcnds  15865  harmonic  15873  arisum  15874  expcnv  15878  geo2sum  15887  geo2lim  15889  geoisum1  15893  geoisum1c  15894  0.999...  15895  mertenslem2  15899  fallfacfwd  16050  0fallfac  16051  0risefac  16052  ef0lem  16092  ege2le3  16104  efaddlem  16107  efexp  16117  rpnnen2lem2  16231  rpnnen2lem4  16233  ruclem12  16257  dvdsmodexp  16278  dvdsexp2im  16344  nn0enne  16394  nnehalf  16396  nno  16399  nn0o  16400  pwp1fsum  16408  divalg2  16422  ndvdssub  16426  gcdmultiplez  16552  gcddiv  16568  rpmulgcd  16574  rplpwr  16575  nn0expgcd  16581  dvdssqlem  16583  eucalgf  16600  lcmflefac  16665  1nprm  16696  2mulprm  16710  isprm5  16724  isprm6  16731  prmdvdsexp  16732  phicl2  16785  phibndlem  16787  phiprmpw  16793  crth  16795  eulerthlem2  16799  hashgcdlem  16805  phisum  16808  pythagtriplem10  16838  pythagtriplem6  16839  pythagtriplem7  16840  pythagtriplem12  16844  pythagtriplem14  16846  pclem  16856  pcexp  16877  pcid  16891  pcprod  16913  pcbc  16918  prmpwdvds  16922  infpnlem1  16928  infpnlem2  16929  prmunb  16932  prmreclem6  16939  1arith  16945  vdwapf  16990  0hashbc  17025  ram0  17040  prmdvdsprmo  17060  prmdvdsprmop  17061  prmolefac  17064  prmgaplem1  17067  prmgaplem2  17068  prmgapprmolem  17079  prmgapprmo  17080  cshwrepswhash1  17120  smndex1n0mnd  18888  ghmmulg  19209  odmodnn0  19519  dfod2  19543  submod  19548  prmirredlem  21431  prmirred  21433  znf1o  21510  znhash  21517  znfi  21518  znfld  21519  znidomb  21520  znunithash  21523  znrrg  21524  frobrhm  21534  cply1mul  22232  cply1coe0  22237  cply1coe0bi  22238  ply1fermltlchr  22248  cpmatmcllem  22654  m2cpm  22677  m2cpminvid2lem  22690  fvmptnn04ifa  22786  chfacfisf  22790  chfacfisfcpmat  22791  chfacffsupp  22792  chfacfscmul0  22794  chfacfscmulfsupp  22795  chfacfscmulgsum  22796  chfacfpmmul0  22798  chfacfpmmulfsupp  22799  chfacfpmmulgsum  22800  chfacfpmmulgsum2  22801  cayhamlem1  22802  cpmadugsumlemF  22812  tgpmulg  24029  cmodscexp  25070  cphipval  25193  ovollb2lem  25439  ovoliunlem1  25453  ovoliunlem3  25455  uniioombllem3  25536  uniioombllem4  25537  opnmbllem  25552  mbfi1fseqlem1  25666  mbfi1fseqlem3  25668  mbfi1fseqlem4  25669  mbfi1fseqlem5  25670  mbfi1fseqlem6  25671  dvexp  25907  dvexp3  25932  idomrootle  26128  plyco  26196  dgrcolem1  26229  plydivex  26255  aaliou3lem2  26301  aaliou3lem3  26302  aaliou3lem5  26305  aaliou3lem6  26306  aaliou3lem7  26307  aaliou3lem9  26308  radcnvlem2  26373  dvradcnv  26380  pserdv2  26390  abelthlem6  26396  abelthlem9  26400  logtayllem  26618  logtayl  26619  logtaylsum  26620  logtayl2  26621  cxproot  26649  root1id  26714  logbgcd1irr  26754  atantayl  26897  atantayl2  26898  leibpilem2  26901  leibpi  26902  birthdaylem2  26912  birthdaylem3  26913  dfef2  26931  basellem2  27042  basellem4  27044  basellem5  27045  basellem6  27046  basellem8  27048  isppw2  27075  vmappw  27076  sqf11  27099  vma1  27126  1sgm2ppw  27161  chtublem  27172  fsumvma2  27175  vmasum  27177  dchrelbas4  27204  dchrzrhcl  27206  dchrfi  27216  dchrhash  27232  pcbcctr  27237  bclbnd  27241  bposlem1  27245  lgsval4a  27280  lgsdchrval  27315  lgsdchr  27316  gausslemma2dlem0c  27319  gausslemma2dlem0d  27320  gausslemma2dlem6  27333  2lgslem1a1  27350  2lgslem1c  27354  2lgslem3a1  27361  2lgslem3b1  27362  2lgslem3c1  27363  2lgslem3d1  27364  2sqreunnlem1  27410  2sqreunnltblem  27412  rplogsumlem2  27446  dchrisumlem2  27451  ostth2lem1  27579  ostth2lem3  27596  ostth3  27599  cusgrsize2inds  29379  pthdivtx  29655  cyclnumvtx  29728  crctcshwlkn0lem4  29741  crctcshwlkn0lem5  29742  crctcshwlkn0lem7  29744  0enwwlksnge1  29792  rusgr0edg  29901  clwlkclwwlkf1lem2  29932  clwlkclwwlkf1lem3  29933  clwwisshclwwslem  29941  clwwlkinwwlk  29967  clwwlkel  29973  clwwlkf  29974  clwwlkf1  29976  clwwlknwwlksnb  29982  wwlksubclwwlk  29985  erclwwlknref  29996  clwwlknonwwlknonb  30033  numclwwlkqhash  30302  numclwwlk2lem1  30303  numclwlk2lem2f  30304  numclwlk2lem2f1o  30306  ipval2  30634  ipasslem3  30760  ipasslem4  30761  nn0min  32745  znfermltl  33327  ply1fermltl  33543  esumcst  34040  eulerpartlemb  34346  fibp1  34379  ballotlem1  34465  subfacp1lem6  35153  subfaclim  35156  subfacval3  35157  snmlff  35297  bcprod  35701  faclim2  35711  nn0prpwlem  36286  knoppndvlem18  36493  opnmbllem0  37626  nnubfi  37720  nninfnub  37721  geomcau  37729  heiborlem5  37785  heiborlem6  37786  heiborlem7  37787  heiborlem8  37788  bfplem1  37792  lcmineqlem12  41999  aks4d1p1p2  42029  primrootscoprmpow  42058  2ap1caineq  42104  dvdsexpnn  42329  dvdsexpnn0  42330  zaddcomlem  42441  fidomncyc  42505  dffltz  42604  fltnltalem  42632  irrapxlem2  42793  pellexlem1  42799  pellexlem5  42803  pellqrex  42849  monotoddzzfi  42913  jm2.17c  42933  acongeq  42954  jm2.18  42959  jm2.23  42967  jm2.26lem3  42972  jm3.1  42991  expdiophlem1  42992  idomodle  43162  proot1ex  43167  rp-isfinite6  43489  cnvtrclfv  43695  cotrclrcl  43713  inductionexd  44126  binomcxplemnotnn0  44328  nnne1ge2  45268  dvnmptconst  45918  stoweidlem3  45980  stoweidlem7  45984  stoweidlem34  46011  wallispilem4  46045  wallispilem5  46046  wallispi2lem1  46048  wallispi2lem2  46049  stirlinglem2  46052  stirlinglem3  46053  stirlinglem4  46054  stirlinglem5  46055  stirlinglem7  46057  stirlinglem11  46061  stirlinglem14  46064  stirlinglem15  46065  stirlingr  46067  fourierdlem15  46099  fourierdlem21  46105  fourierdlem22  46106  fourierdlem92  46175  fourierdlem112  46195  fouriersw  46208  sge0rpcpnf  46398  sge0ad2en  46408  ovnsubaddlem1  46547  ovnsubaddlem2  46548  ovolval5lem1  46629  ovolval5lem2  46630  ceilhalfelfzo1  47307  iccpartiltu  47384  iccpartigtl  47385  iccpartlt  47386  iccpartleu  47390  iccpartrn  47392  iccelpart  47395  iccpartiun  47396  iccpartdisj  47399  sqrtpwpw2p  47500  fmtnosqrt  47501  odz2prm2pw  47525  fmtnoprmfac1lem  47526  fmtnoprmfac1  47527  2pwp1prm  47551  lighneallem1  47567  lighneallem2  47568  lighneallem3  47569  lighneallem4a  47570  lighneallem4  47572  nnpw2evenALTV  47664  dfwppr  47700  gpgorder  48011  gpgedgvtx0  48013  gpgedgvtx1  48014  cznabel  48183  cznrng  48184  ztprmneprm  48270  altgsumbc  48275  altgsumbcALT  48276  pw2m1lepw2m1  48444  nneom  48455  logbpw2m1  48495  blennn  48503  blenpw2m1  48507  blengt1fldiv2p1  48521  dignn0ldlem  48530  dignnld  48531  dig2nn1st  48533  dignn0flhalflem1  48543  nn0sumshdiglemA  48547  nn0sumshdiglemB  48548  itcovalt2lem2lem1  48601  eenglngeehlnm  48667