Theorem nnnn0 10878

Description: A positive integer is a nonnegative integer. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nnnn0	|- ( A e. NN -> A e. NN0 )

Proof of Theorem nnnn0

Step	Hyp	Ref	Expression
1		nnssnn0 10874	. 2 |- NN C_ NN0
2	1	sseli 3461	1 |- ( A e. NN -> A e. NN0 )

Syntax hints:   -> wi 4   e. wcel 1869   NNcn 10611   NN0cn0 10871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-un 3442  df-in 3444  df-ss 3451  df-n0 10872

This theorem is referenced by:  nnnn0i  10879  elnnnn0b  10916  elnnnn0c  10917  elz2  10956  nn0ind-raph  11037  zindd  11038  fzo1fzo0n0  11959  ubmelfzo  11980  elfzom1elp1fzo  11982  fzo0sn0fzo1  12002  quoremnn0ALT  12085  modmulnn  12115  expneg  12281  expcllem  12284  expcl2lem  12285  expeq0  12303  mulexpz  12313  expnlbnd  12403  expmulnbnd  12405  digit2  12406  digit1  12407  facmapnn  12471  facdiv  12473  faclbnd  12476  faclbnd3  12478  faclbnd4lem3  12481  faclbnd4lem4  12482  faclbnd5  12484  faclbnd6  12485  bcval5  12504  ishashinf  12625  iswrdi  12673  swrdn0  12782  swrdtrcfv  12793  swrdccatwrd  12820  repswfsts  12880  repswlsw  12881  repswcshw  12907  relexpnnrn  13102  relexpaddg  13110  absexpz  13362  isercoll  13724  summolem3  13773  summolem2a  13774  climcndslem2  13901  climcnds  13902  harmonic  13910  arisum  13911  expcnv  13915  geo2sum  13922  geo2lim  13924  geoisum1  13928  geoisum1c  13929  0.999...  13930  mertenslem2  13934  fallfacfwd  14082  0fallfac  14083  0risefac  14084  ef0lem  14126  ege2le3  14137  efaddlem  14140  efexp  14148  rpnnen2lem2  14261  rpnnen2lem4  14263  ruclem12  14286  divalg2  14379  ndvdssub  14381  gcddiv  14510  gcdmultiple  14511  gcdmultiplez  14512  rpmulgcd  14516  rplpwr  14517  dvdssqlem  14520  eucalgf  14535  lcmslefacOLD  14579  lcmflefac  14614  1nprm  14622  isprm5  14644  isprm6  14659  prmdvdsexp  14660  phicl2  14709  phibndlem  14711  phiprmpw  14717  crt  14719  eulerthlem2  14723  pythagtriplem10  14763  pythagtriplem6  14764  pythagtriplem7  14765  pythagtriplem12  14769  pythagtriplem14  14771  pclem  14781  pcexp  14802  pcid  14815  pcprod  14833  pcbc  14838  prmpwdvds  14841  infpnlem1  14847  infpnlem2  14848  prmunb  14851  prmreclem6  14858  1arith  14864  vdwapf  14915  0hashbc  14952  ram0  14973  prmdvdsprmo  14993  prmdvdsprmop  14994  prmolefac  14997  prmgaplem1  15000  prmgaplem2  15001  prmorlefacOLD  15011  prmgapprmolem  15025  prmgapprmo  15026  cshwrepswhash1  15066  ghmmulg  16888  odmodnn0  17182  dfod2  17208  submod  17211  cply1mul  18880  cply1coe0  18886  cply1coe0bi  18887  prmirredlem  19056  prmirred  19058  znf1o  19114  znhash  19121  znfi  19122  znfld  19123  znidomb  19124  znunithash  19127  znrrg  19128  cpmatmcllem  19734  m2cpm  19757  m2cpminvid2lem  19770  fvmptnn04ifa  19866  chfacfisf  19870  chfacfisfcpmat  19871  chfacffsupp  19872  chfacfscmul0  19874  chfacfscmulfsupp  19875  chfacfscmulgsum  19876  chfacfpmmul0  19878  chfacfpmmulfsupp  19879  chfacfpmmulgsum  19880  chfacfpmmulgsum2  19881  cayhamlem1  19882  cpmadugsumlemF  19892  tgpmulg  21100  ovollb2lem  22433  ovoliunlem1  22447  ovoliunlem3  22449  uniioombllem3  22535  uniioombllem4  22536  opnmbllem  22551  mbfi1fseqlem1  22665  mbfi1fseqlem3  22667  mbfi1fseqlem4  22668  mbfi1fseqlem5  22669  mbfi1fseqlem6  22670  dvexp  22899  dvexp3  22922  plyco  23187  dgrcolem1  23219  plydivex  23242  aaliou3lem2  23291  aaliou3lem3  23292  aaliou3lem5  23295  aaliou3lem6  23296  aaliou3lem7  23297  aaliou3lem9  23298  radcnvlem2  23361  dvradcnv  23368  pserdv2  23377  abelthlem6  23383  abelthlem9  23387  logtayllem  23596  logtayl  23597  logtaylsum  23598  logtayl2  23599  cxproot  23627  root1id  23686  atantayl  23855  atantayl2  23856  leibpilem2  23859  leibpi  23860  birthdaylem2  23870  birthdaylem3  23871  dfef2  23888  basellem2  24000  basellem4  24002  basellem5  24003  basellem6  24004  basellem8  24006  isppw2  24034  vmappw  24035  sqf11  24058  vma1  24085  1sgm2ppw  24120  chtublem  24131  fsumvma2  24134  vmasum  24136  dchrelbas4  24163  dchrzrhcl  24165  dchrfi  24175  dchrhash  24191  pcbcctr  24196  bclbnd  24200  bposlem1  24204  lgsval4a  24238  lgsdchrval  24267  lgsdchr  24268  rplogsumlem2  24315  dchrisumlem2  24320  ostth2lem1  24448  ostth2lem3  24465  ostth3  24468  cusgrasize2inds  25197  cyclnspth  25351  clwwlkel  25513  clwwlkf  25514  clwwlkf1  25516  wwlksubclwwlk  25524  clwwisshclwwlem  25526  clwlkf1clwwlklem  25569  rusgra0edg  25675  clwlknclwlkdifnum  25681  clwwlkextfrlem1  25796  numclwwlkqhash  25820  numclwwlk2lem1  25822  numclwlk2lem2f  25823  numclwlk2lem2f1o  25825  gxcl  25985  ipval2  26335  ipasslem3  26466  ipasslem4  26467  nn0min  28385  esumcst  28886  eulerpartlemb  29203  fibp1  29236  ballotlem1  29321  subfacp1lem6  29910  subfaclim  29913  subfacval3  29914  snmlff  30054  bcprod  30375  faclim2  30385  dvdspw  30387  nn0prpwlem  30977  opnmbllem0  31896  nnubfi  31999  nninfnub  32000  geomcau  32008  heiborlem5  32067  heiborlem6  32068  heiborlem7  32069  heiborlem8  32070  bfplem1  32074  irrapxlem2  35593  pellexlem1  35599  pellexlem5  35603  pellqrex  35652  monotoddzzfi  35716  expmordi  35721  rpexpmord  35722  jm2.17c  35738  acongeq  35759  jm2.18  35769  jm2.23  35777  jm2.26lem3  35782  jm3.1  35801  expdiophlem1  35802  idomrootle  35995  idomodle  35996  hashgcdlem  36000  phisum  36002  proot1ex  36004  rp-isfinite6  36089  cnvtrclfv  36182  cotrclrcl  36200  inductionexd  36457  binomcxplemnotnn0  36569  nnne1ge2  37353  dvnmptconst  37642  stoweidlem3  37689  stoweidlem7  37693  stoweidlem34  37721  wallispilem4  37756  wallispilem5  37757  wallispi2lem1  37759  wallispi2lem2  37760  stirlinglem2  37763  stirlinglem3  37764  stirlinglem4  37765  stirlinglem5  37766  stirlinglem7  37768  stirlinglem11  37772  stirlinglem14  37775  stirlinglem15  37776  stirlingr  37778  fourierdlem15  37810  fourierdlem21  37816  fourierdlem22  37817  fourierdlem92  37888  fourierdlem112  37908  fouriersw  37921  sge0rpcpnf  38057  sge0ad2en  38067  ovnsubaddlem1  38173  ovnsubaddlem2  38174  iccpartiltu  38454  iccpartigtl  38455  iccpartlt  38456  iccpartleu  38460  iccpartrn  38462  iccelpart  38465  iccpartiun  38466  iccpartdisj  38469  nnpw2evenALTV  38547  pfxn0  38653  cznabel  39260  cznrng  39261  ztprmneprm  39434  altgsumbc  39439  altgsumbcALT  39440  pw2m1lepw2m1  39624  nn0enne  39632  nno  39634  nn0o  39635  nneom  39640  logbpw2m1  39684  blennn  39692  blenpw2m1  39696  blengt1fldiv2p1  39710  dignn0ldlem  39719  dignnld  39720  dig2nn1st  39722  dignn0flhalflem1  39732  nn0sumshdiglemA  39736  nn0sumshdiglemB  39737