Theorem nnnn0 10578

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

Syntax hints:   -> wi 4   e. wcel 1756   NNcn 10314   NN0cn0 10571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-un 3328  df-in 3330  df-ss 3337  df-n0 10572

This theorem is referenced by:  nnnn0i  10579  elnnnn0b  10616  elnnnn0c  10617  elz2  10655  nn0ind-raph  10734  zindd  10735  fzo1fzo0n0  11580  ubmelfzo  11595  fzo0sn0fzo1  11609  quoremnn0ALT  11688  modmulnn  11717  expneg  11865  expcllem  11868  expcl2lem  11869  expeq0  11886  mulexpz  11896  expnlbnd  11986  expmulnbnd  11988  digit2  11989  digit1  11990  facdiv  12055  faclbnd  12058  faclbnd3  12060  faclbnd4lem3  12063  faclbnd4lem4  12064  faclbnd5  12066  faclbnd6  12067  bcval5  12086  iswrdi  12231  swrdn0  12316  swrdtrcfv  12329  swrdccatwrd  12354  wrdeqcats1  12360  repswfsts  12411  repswlsw  12412  repswcshw  12438  absexpz  12786  isercoll  13137  summolem3  13183  summolem2a  13184  climcndslem2  13305  climcnds  13306  harmonic  13313  arisum  13314  expcnv  13318  geo2sum  13325  geo2lim  13327  geoisum1  13331  geoisum1c  13332  0.999...  13333  mertenslem2  13337  ef0lem  13356  ege2le3  13367  efaddlem  13370  efexp  13377  xpnnenOLD  13484  rpnnen2lem2  13490  rpnnen2lem4  13492  ruclem12  13515  divalg2  13601  ndvdssub  13603  gcddiv  13725  gcdmultiple  13726  gcdmultiplez  13727  rpmulgcd  13731  rplpwr  13732  dvdssqlem  13735  eucalgf  13750  1nprm  13760  isprm6  13787  isprm5  13790  prmdvdsexp  13792  phicl2  13835  phibndlem  13837  phiprmpw  13843  crt  13845  eulerthlem2  13849  pythagtriplem10  13879  pythagtriplem6  13880  pythagtriplem7  13881  pythagtriplem12  13885  pythagtriplem14  13887  pclem  13897  pcexp  13918  pcid  13931  pcprod  13949  pcbc  13954  prmpwdvds  13957  infpnlem1  13963  infpnlem2  13964  prmunb  13967  prmreclem6  13974  1arith  13980  vdwapf  14025  0hashbc  14060  ram0  14075  cshwrepswhash1  14121  ghmmulg  15750  odmodnn0  16034  dfod2  16056  submod  16059  prmirredlem  17892  prmirred  17894  prmirredlemOLD  17895  prmirredOLD  17897  znf1o  17959  znhash  17966  znfi  17967  znfld  17968  znidomb  17969  znunithash  17972  znrrg  17973  tgpmulg  19639  ovollb2lem  20946  ovoliunlem1  20960  ovoliunlem3  20962  uniioombllem3  21040  uniioombllem4  21041  opnmbllem  21056  mbfi1fseqlem1  21168  mbfi1fseqlem3  21170  mbfi1fseqlem4  21171  mbfi1fseqlem5  21172  mbfi1fseqlem6  21173  dvexp  21402  dvexp3  21425  plyco  21684  dgrcolem1  21715  plydivex  21738  aaliou3lem2  21784  aaliou3lem3  21785  aaliou3lem5  21788  aaliou3lem6  21789  aaliou3lem7  21790  aaliou3lem9  21791  radcnvlem2  21854  dvradcnv  21861  pserdv2  21870  abelthlem6  21876  abelthlem9  21880  logtayllem  22079  logtayl  22080  logtaylsum  22081  logtayl2  22082  cxproot  22110  root1id  22167  atantayl  22307  atantayl2  22308  leibpilem2  22311  leibpi  22312  birthdaylem2  22321  birthdaylem3  22322  dfef2  22339  basellem2  22394  basellem4  22396  basellem5  22397  basellem6  22398  basellem8  22400  isppw2  22428  vmappw  22429  sqf11  22452  vma1  22479  1sgm2ppw  22514  chtublem  22525  fsumvma2  22528  vmasum  22530  dchrelbas4  22557  dchrzrhcl  22559  dchrfi  22569  dchrhash  22585  pcbcctr  22590  bclbnd  22594  bposlem1  22598  lgsval4a  22632  lgsdchrval  22661  lgsdchr  22662  rplogsumlem2  22709  dchrisumlem2  22714  ostth2lem1  22842  ostth2lem3  22859  ostth3  22862  cusgrasize2inds  23336  cyclnspth  23468  gxcl  23703  ipval2  24053  ipasslem3  24184  ipasslem4  24185  ishashinf  26036  nn0min  26041  esumcst  26466  eulerpartlemb  26703  fibp1  26736  ballotlem1  26821  subfacp1lem6  27025  subfaclim  27028  subfacval3  27029  snmlff  27170  fallfacfwd  27490  0fallfac  27491  0risefac  27492  faclim2  27505  dvdspw  27507  opnmbllem0  28380  nn0prpwlem  28470  nnubfi  28599  nninfnub  28600  geomcau  28608  heiborlem5  28667  heiborlem6  28668  heiborlem7  28669  heiborlem8  28670  bfplem1  28674  irrapxlem2  29117  pellexlem1  29123  pellexlem5  29127  pellqrex  29173  monotoddzzfi  29236  expmordi  29241  rpexpmord  29242  jm2.17c  29258  acongeq  29279  jm2.18  29290  jm2.23  29298  jm2.26lem3  29303  jm3.1  29322  expdiophlem1  29323  idomrootle  29513  idomodle  29514  hashgcdlem  29518  phisum  29520  proot1ex  29522  stoweidlem3  29751  stoweidlem7  29755  stoweidlem34  29782  wallispilem4  29816  wallispilem5  29817  wallispi2lem1  29819  wallispi2lem2  29820  stirlinglem2  29823  stirlinglem3  29824  stirlinglem4  29825  stirlinglem5  29826  stirlinglem7  29828  stirlinglem11  29832  stirlinglem14  29835  stirlinglem15  29836  stirlingr  29838  clwwlkel  30408  clwwlkf  30409  clwwlkf1  30411  wwlksubclwwlk  30419  clwwisshclwwlem  30423  clwlkf1clwwlklem  30475  rusgra0edg  30526  clwlknclwlkdifnum  30532  clwwlkextfrlem1  30622  numclwwlkqhash  30646  numclwwlk2lem1  30648  numclwlk2lem2f  30649  numclwlk2lem2f1o  30651  ztprmneprm  30691  altgsumbc  30700  altgsumbcALT  30701