Theorem nnnn0 10574

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 10570	. 2 |- NN C_ NN0
2	1	sseli 3340	1 |- ( A e. NN -> A e. NN0 )

Syntax hints:   -> wi 4   e. wcel 1755   NNcn 10310   NN0cn0 10567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-un 3321  df-in 3323  df-ss 3330  df-n0 10568

This theorem is referenced by:  nnnn0i  10575  elnnnn0b  10612  elnnnn0c  10613  elz2  10651  nn0ind-raph  10730  zindd  10731  fzo1fzo0n0  11572  ubmelfzo  11587  fzo0sn0fzo1  11601  quoremnn0ALT  11680  modmulnn  11709  expneg  11857  expcllem  11860  expcl2lem  11861  expeq0  11878  mulexpz  11888  expnlbnd  11978  expmulnbnd  11980  digit2  11981  digit1  11982  facdiv  12047  faclbnd  12050  faclbnd3  12052  faclbnd4lem3  12055  faclbnd4lem4  12056  faclbnd5  12058  faclbnd6  12059  bcval5  12078  iswrdi  12223  swrdn0  12308  swrdtrcfv  12321  swrdccatwrd  12346  wrdeqcats1  12352  repswfsts  12403  repswlsw  12404  repswcshw  12430  absexpz  12778  isercoll  13129  summolem3  13175  summolem2a  13176  climcndslem2  13296  climcnds  13297  harmonic  13304  arisum  13305  expcnv  13309  geo2sum  13316  geo2lim  13318  geoisum1  13322  geoisum1c  13323  0.999...  13324  mertenslem2  13328  ef0lem  13347  ege2le3  13358  efaddlem  13361  efexp  13368  xpnnenOLD  13475  rpnnen2lem2  13481  rpnnen2lem4  13483  ruclem12  13506  divalg2  13592  ndvdssub  13594  gcddiv  13716  gcdmultiple  13717  gcdmultiplez  13718  rpmulgcd  13722  rplpwr  13723  dvdssqlem  13726  eucalgf  13741  1nprm  13751  isprm6  13778  isprm5  13781  prmdvdsexp  13783  phicl2  13826  phibndlem  13828  phiprmpw  13834  crt  13836  eulerthlem2  13840  pythagtriplem10  13870  pythagtriplem6  13871  pythagtriplem7  13872  pythagtriplem12  13876  pythagtriplem14  13878  pclem  13888  pcexp  13909  pcid  13922  pcprod  13940  pcbc  13945  prmpwdvds  13948  infpnlem1  13954  infpnlem2  13955  prmunb  13958  prmreclem6  13965  1arith  13971  vdwapf  14016  0hashbc  14051  ram0  14066  cshwrepswhash1  14112  ghmmulg  15739  odmodnn0  16023  dfod2  16045  submod  16048  prmirredlem  17759  prmirred  17761  prmirredlemOLD  17762  prmirredOLD  17764  znf1o  17826  znhash  17833  znfi  17834  znfld  17835  znidomb  17836  znunithash  17839  znrrg  17840  tgpmulg  19506  ovollb2lem  20813  ovoliunlem1  20827  ovoliunlem3  20829  uniioombllem3  20907  uniioombllem4  20908  opnmbllem  20923  mbfi1fseqlem1  21035  mbfi1fseqlem3  21037  mbfi1fseqlem4  21038  mbfi1fseqlem5  21039  mbfi1fseqlem6  21040  dvexp  21269  dvexp3  21292  plyco  21594  dgrcolem1  21625  plydivex  21648  aaliou3lem2  21694  aaliou3lem3  21695  aaliou3lem5  21698  aaliou3lem6  21699  aaliou3lem7  21700  aaliou3lem9  21701  radcnvlem2  21764  dvradcnv  21771  pserdv2  21780  abelthlem6  21786  abelthlem9  21790  logtayllem  21989  logtayl  21990  logtaylsum  21991  logtayl2  21992  cxproot  22020  root1id  22077  atantayl  22217  atantayl2  22218  leibpilem2  22221  leibpi  22222  birthdaylem2  22231  birthdaylem3  22232  dfef2  22249  basellem2  22304  basellem4  22306  basellem5  22307  basellem6  22308  basellem8  22310  isppw2  22338  vmappw  22339  sqf11  22362  vma1  22389  1sgm2ppw  22424  chtublem  22435  fsumvma2  22438  vmasum  22440  dchrelbas4  22467  dchrzrhcl  22469  dchrfi  22479  dchrhash  22495  pcbcctr  22500  bclbnd  22504  bposlem1  22508  lgsval4a  22542  lgsdchrval  22571  lgsdchr  22572  rplogsumlem2  22619  dchrisumlem2  22624  ostth2lem1  22752  ostth2lem3  22769  ostth3  22772  cusgrasize2inds  23208  cyclnspth  23340  gxcl  23575  ipval2  23925  ipasslem3  24056  ipasslem4  24057  ishashinf  25908  nn0min  25913  esumcst  26368  eulerpartlemb  26599  fibp1  26632  ballotlem1  26717  subfacp1lem6  26921  subfaclim  26924  subfacval3  26925  snmlff  27066  fallfacfwd  27386  0fallfac  27387  0risefac  27388  faclim2  27401  dvdspw  27403  opnmbllem0  28271  nn0prpwlem  28361  nnubfi  28490  nninfnub  28491  geomcau  28499  heiborlem5  28558  heiborlem6  28559  heiborlem7  28560  heiborlem8  28561  bfplem1  28565  irrapxlem2  29009  pellexlem1  29015  pellexlem5  29019  pellqrex  29065  monotoddzzfi  29128  expmordi  29133  rpexpmord  29134  jm2.17c  29150  acongeq  29171  jm2.18  29182  jm2.23  29190  jm2.26lem3  29195  jm3.1  29214  expdiophlem1  29215  idomrootle  29405  idomodle  29406  hashgcdlem  29410  phisum  29412  proot1ex  29414  stoweidlem3  29644  stoweidlem7  29648  stoweidlem34  29675  wallispilem4  29709  wallispilem5  29710  wallispi2lem1  29712  wallispi2lem2  29713  stirlinglem2  29716  stirlinglem3  29717  stirlinglem4  29718  stirlinglem5  29719  stirlinglem7  29721  stirlinglem11  29725  stirlinglem14  29728  stirlinglem15  29729  stirlingr  29731  clwwlkel  30301  clwwlkf  30302  clwwlkf1  30304  wwlksubclwwlk  30312  clwwisshclwwlem  30316  clwlkf1clwwlklem  30368  rusgra0edg  30419  clwlknclwlkdifnum  30425  clwwlkextfrlem1  30515  numclwwlkqhash  30539  numclwwlk2lem1  30541  numclwlk2lem2f  30542  numclwlk2lem2f1o  30544  ztprmneprm  30583