Theorem nnnn0 12502

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

Syntax hints:   → wi 4   ∈ wcel 2145  ℕcn 12224  ℕ₀cn0 12495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924  df-n0 12496

This theorem is referenced by:  nnnn0i  12503  elnnnn0b  12539  elnnnn0c  12540  elz2  12600  nn0ind-raph  12687  zindd  12688  fzo1fzo0n0  13735  ubmelfzo  13750  elfzom1elp1fzo  13752  fzo0sn0fzo1  13775  quoremnn0ALT  13881  modmulnn  13913  modsumfzodifsn  13971  addmodlteq  13973  expneg  14096  expcllem  14099  expcl2lem  14100  expeq0  14119  mulexpz  14129  expmordi  14194  rpexpmord  14195  expnlbnd  14260  expmulnbnd  14262  digit2  14263  digit1  14264  facmapnn  14312  facdiv  14314  faclbnd  14317  faclbnd3  14319  faclbnd4lem3  14322  faclbnd4lem4  14323  faclbnd5  14325  faclbnd6  14326  bcval5  14345  ishashinf  14490  iswrdi  14544  pfxn0  14714  repswfsts  14808  repswlsw  14809  repswcshw  14839  relexpnnrn  15072  relexpaddg  15080  absexpz  15346  isercoll  15709  summolem3  15755  summolem2a  15756  climcndslem2  15894  climcnds  15895  harmonic  15903  arisum  15904  expcnv  15908  geo2sum  15917  geo2lim  15919  geoisum1  15923  geoisum1c  15924  0.999...  15925  mertenslem2  15929  fallfacfwd  16080  0fallfac  16081  0risefac  16082  ef0lem  16122  ege2le3  16134  efaddlem  16137  efexp  16147  rpnnen2lem2  16261  rpnnen2lem4  16263  ruclem12  16287  dvdsmodexp  16308  dvdsexp2im  16375  nn0enne  16425  nnehalf  16427  nno  16430  nn0o  16431  pwp1fsum  16439  divalg2  16453  ndvdssub  16457  gcdmultiplez  16583  gcddiv  16599  rpmulgcd  16605  rplpwr  16606  nn0expgcd  16612  dvdssqlem  16614  eucalgf  16631  lcmflefac  16696  1nprm  16727  2mulprm  16741  isprm5  16756  isprm6  16763  prmdvdsexp  16764  phicl2  16817  phibndlem  16819  phiprmpw  16825  crth  16827  eulerthlem2  16831  hashgcdlem  16837  phisum  16840  pythagtriplem10  16870  pythagtriplem6  16871  pythagtriplem7  16872  pythagtriplem12  16876  pythagtriplem14  16878  pclem  16888  pcexp  16909  pcid  16923  pcprod  16945  pcbc  16950  prmpwdvds  16954  infpnlem1  16960  infpnlem2  16961  prmunb  16964  prmreclem6  16971  1arith  16977  vdwapf  17022  0hashbc  17057  ram0  17072  prmdvdsprmo  17092  prmdvdsprmop  17093  prmolefac  17096  prmgaplem1  17099  prmgaplem2  17100  prmgapprmolem  17111  prmgapprmo  17112  cshwrepswhash1  17152  smndex1n0mnd  18964  ghmmulg  19289  odmodnn0  19601  dfod2  19625  submod  19630  prmirredlem  21582  prmirred  21584  znf1o  21661  znhash  21668  znfi  21669  znfld  21670  znidomb  21671  znunithash  21674  znrrg  21675  frobrhm  21685  cply1mul  22417  cply1coe0  22422  cply1coe0bi  22423  ply1fermltlchr  22433  cpmatmcllem  22836  m2cpm  22859  m2cpminvid2lem  22872  fvmptnn04ifa  22968  chfacfisf  22972  chfacfisfcpmat  22973  chfacffsupp  22974  chfacfscmul0  22976  chfacfscmulfsupp  22977  chfacfscmulgsum  22978  chfacfpmmul0  22980  chfacfpmmulfsupp  22981  chfacfpmmulgsum  22982  chfacfpmmulgsum2  22983  cayhamlem1  22984  cpmadugsumlemF  22994  tgpmulg  24211  cmodscexp  25241  cphipval  25363  ovollb2lem  25608  ovoliunlem1  25622  ovoliunlem3  25624  uniioombllem3  25705  uniioombllem4  25706  opnmbllem  25721  mbfi1fseqlem1  25835  mbfi1fseqlem3  25837  mbfi1fseqlem4  25838  mbfi1fseqlem5  25839  mbfi1fseqlem6  25840  dvexp  26073  dvexp3  26098  idomrootle  26291  plyco  26359  dgrcolem1  26391  plydivex  26419  aaliou3lem2  26465  aaliou3lem3  26466  aaliou3lem5  26469  aaliou3lem6  26470  aaliou3lem7  26471  aaliou3lem9  26472  radcnvlem2  26535  dvradcnv  26542  pserdv2  26551  abelthlem6  26557  abelthlem9  26561  logtayllem  26782  logtayl  26783  logtaylsum  26784  logtayl2  26785  cxproot  26813  root1id  26877  logbgcd1irr  26917  atantayl  27060  atantayl2  27061  leibpilem2  27064  leibpi  27065  birthdaylem2  27075  birthdaylem3  27076  dfef2  27093  basellem2  27204  basellem4  27206  basellem5  27207  basellem6  27208  basellem8  27210  isppw2  27237  vmappw  27238  sqf11  27261  vma1  27288  1sgm2ppw  27322  chtublem  27333  fsumvma2  27336  vmasum  27338  dchrelbas4  27365  dchrzrhcl  27367  dchrfi  27377  dchrhash  27393  pcbcctr  27398  bclbnd  27402  bposlem1  27406  lgsval4a  27441  lgsdchrval  27476  lgsdchr  27477  gausslemma2dlem0c  27480  gausslemma2dlem0d  27481  gausslemma2dlem6  27494  2lgslem1a1  27511  2lgslem1c  27515  2lgslem3a1  27522  2lgslem3b1  27523  2lgslem3c1  27524  2lgslem3d1  27525  2sqreunnlem1  27571  2sqreunnltblem  27573  rplogsumlem2  27607  dchrisumlem2  27612  ostth2lem1  27740  ostth2lem3  27757  ostth3  27760  cusgrsize2inds  29712  pthdivtx  29985  cyclnumvtx  30058  crctcshwlkn0lem4  30071  crctcshwlkn0lem5  30072  crctcshwlkn0lem7  30074  0enwwlksnge1  30122  rusgr0edg  30234  clwlkclwwlkf1lem2  30265  clwlkclwwlkf1lem3  30266  clwwisshclwwslem  30274  clwwlkinwwlk  30300  clwwlkel  30306  clwwlkf  30307  clwwlkf1  30309  clwwlknwwlksnb  30315  wwlksubclwwlk  30318  erclwwlknref  30329  clwwlknonwwlknonb  30366  numclwwlkqhash  30635  numclwwlk2lem1  30636  numclwlk2lem2f  30637  numclwlk2lem2f1o  30639  ipval2  30968  ipasslem3  31094  ipasslem4  31095  nn0min  33078  znfermltl  33596  ply1fermltl  33793  esumcst  34370  eulerpartlemb  34675  fibp1  34708  ballotlem1  34794  subfacp1lem6  35548  subfaclim  35551  subfacval3  35552  snmlff  35692  bcprod  36101  faclim2  36111  nn0prpwlem  36695  knoppndvlem18  36980  opnmbllem0  38167  nnubfi  38261  nninfnub  38262  geomcau  38270  heiborlem5  38326  heiborlem6  38327  heiborlem7  38328  heiborlem8  38329  bfplem1  38333  lcmineqlem12  42669  aks4d1p1p2  42699  primrootscoprmpow  42728  2ap1caineq  42774  dvdsexpnn  42954  dvdsexpnn0  42955  zaddcomlem  43097  fidomncyc  43165  dffltz  43228  fltnltalem  43256  irrapxlem2  43412  pellexlem1  43418  pellexlem5  43422  pellqrex  43468  monotoddzzfi  43531  jm2.17c  43551  acongeq  43572  jm2.18  43577  jm2.23  43585  jm2.26lem3  43590  jm3.1  43609  expdiophlem1  43610  idomodle  43780  proot1ex  43785  rp-isfinite6  44106  cnvtrclfv  44312  cotrclrcl  44330  inductionexd  44743  binomcxplemnotnn0  44930  nnne1ge2  45868  dvnmptconst  46513  stoweidlem3  46575  stoweidlem7  46579  stoweidlem34  46606  wallispilem4  46640  wallispilem5  46641  wallispi2lem1  46643  wallispi2lem2  46644  stirlinglem2  46647  stirlinglem3  46648  stirlinglem4  46649  stirlinglem5  46650  stirlinglem7  46652  stirlinglem11  46656  stirlinglem14  46659  stirlinglem15  46660  stirlingr  46662  fourierdlem15  46694  fourierdlem21  46700  fourierdlem22  46701  fourierdlem92  46770  fourierdlem112  46790  fouriersw  46803  sge0rpcpnf  46993  sge0ad2en  47003  ovnsubaddlem1  47142  ovnsubaddlem2  47143  ovolval5lem1  47224  ovolval5lem2  47225  nthrucw  47460  ceilhalfelfzo1  47926  modlt0b  47961  muldvdsfacm1  47979  iccpartiltu  48026  iccpartigtl  48027  iccpartlt  48028  iccpartleu  48032  iccpartrn  48034  iccelpart  48037  iccpartiun  48038  iccpartdisj  48041  sqrtpwpw2p  48145  fmtnosqrt  48146  odz2prm2pw  48170  fmtnoprmfac1lem  48171  fmtnoprmfac1  48172  2pwp1prm  48196  lighneallem1  48212  lighneallem2  48213  lighneallem3  48214  lighneallem4a  48215  lighneallem4  48217  nnpw2evenALTV  48322  dfwppr  48358  gpgorder  48679  gpgedgvtx0  48681  gpgedgvtx1  48682  cznabel  48880  cznrng  48881  ztprmneprm  48978  altgsumbc  48983  altgsumbcALT  48984  pw2m1lepw2m1  49151  nneom  49158  logbpw2m1  49198  blennn  49206  blenpw2m1  49210  blengt1fldiv2p1  49224  dignn0ldlem  49233  dignnld  49234  dig2nn1st  49236  dignn0flhalflem1  49246  nn0sumshdiglemA  49250  nn0sumshdiglemB  49251  itcovalt2lem2lem1  49304  eenglngeehlnm  49370