Theorem nnnn0 10798

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

Syntax hints:   -> wi 4   e. wcel 1767   NNcn 10532   NN0cn0 10791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-in 3483  df-ss 3490  df-n0 10792

This theorem is referenced by:  nnnn0i  10799  elnnnn0b  10836  elnnnn0c  10837  elz2  10877  nn0ind-raph  10957  zindd  10958  fzo1fzo0n0  11828  ubmelfzo  11845  elfzom1elp1fzo  11847  fzo0sn0fzo1  11866  quoremnn0ALT  11947  modmulnn  11976  expneg  12137  expcllem  12140  expcl2lem  12141  expeq0  12158  mulexpz  12168  expnlbnd  12258  expmulnbnd  12260  digit2  12261  digit1  12262  facdiv  12327  faclbnd  12330  faclbnd3  12332  faclbnd4lem3  12335  faclbnd4lem4  12336  faclbnd5  12338  faclbnd6  12339  bcval5  12358  iswrdi  12512  swrdn0  12612  swrdtrcfv  12625  swrdccatwrd  12650  wrdeqcats1  12656  repswfsts  12710  repswlsw  12711  repswcshw  12737  absexpz  13095  isercoll  13446  summolem3  13492  summolem2a  13493  climcndslem2  13618  climcnds  13619  harmonic  13626  arisum  13627  expcnv  13631  geo2sum  13638  geo2lim  13640  geoisum1  13644  geoisum1c  13645  0.999...  13646  mertenslem2  13650  ef0lem  13669  ege2le3  13680  efaddlem  13683  efexp  13690  xpnnenOLD  13797  rpnnen2lem2  13803  rpnnen2lem4  13805  ruclem12  13828  divalg2  13915  ndvdssub  13917  gcddiv  14039  gcdmultiple  14040  gcdmultiplez  14041  rpmulgcd  14045  rplpwr  14046  dvdssqlem  14049  eucalgf  14064  1nprm  14074  isprm6  14102  isprm5  14105  prmdvdsexp  14107  phicl2  14150  phibndlem  14152  phiprmpw  14158  crt  14160  eulerthlem2  14164  pythagtriplem10  14196  pythagtriplem6  14197  pythagtriplem7  14198  pythagtriplem12  14202  pythagtriplem14  14204  pclem  14214  pcexp  14235  pcid  14248  pcprod  14266  pcbc  14271  prmpwdvds  14274  infpnlem1  14280  infpnlem2  14281  prmunb  14284  prmreclem6  14291  1arith  14297  vdwapf  14342  0hashbc  14377  ram0  14392  cshwrepswhash1  14438  ghmmulg  16071  odmodnn0  16357  dfod2  16379  submod  16382  cply1mul  18103  cply1coe0  18109  cply1coe0bi  18110  prmirredlem  18287  prmirred  18289  prmirredlemOLD  18290  prmirredOLD  18292  znf1o  18354  znhash  18361  znfi  18362  znfld  18363  znidomb  18364  znunithash  18367  znrrg  18368  cpmatmcllem  18983  m2cpm  19006  m2cpminvid2lem  19019  fvmptnn04ifa  19115  chfacfisf  19119  chfacfisfcpmat  19120  chfacffsupp  19121  chfacfscmul0  19123  chfacfscmulfsupp  19124  chfacfscmulgsum  19125  chfacfpmmul0  19127  chfacfpmmulfsupp  19128  chfacfpmmulgsum  19129  chfacfpmmulgsum2  19130  cayhamlem1  19131  cpmadugsumlemF  19141  tgpmulg  20324  ovollb2lem  21631  ovoliunlem1  21645  ovoliunlem3  21647  uniioombllem3  21726  uniioombllem4  21727  opnmbllem  21742  mbfi1fseqlem1  21854  mbfi1fseqlem3  21856  mbfi1fseqlem4  21857  mbfi1fseqlem5  21858  mbfi1fseqlem6  21859  dvexp  22088  dvexp3  22111  plyco  22370  dgrcolem1  22401  plydivex  22424  aaliou3lem2  22470  aaliou3lem3  22471  aaliou3lem5  22474  aaliou3lem6  22475  aaliou3lem7  22476  aaliou3lem9  22477  radcnvlem2  22540  dvradcnv  22547  pserdv2  22556  abelthlem6  22562  abelthlem9  22566  logtayllem  22765  logtayl  22766  logtaylsum  22767  logtayl2  22768  cxproot  22796  root1id  22853  atantayl  22993  atantayl2  22994  leibpilem2  22997  leibpi  22998  birthdaylem2  23007  birthdaylem3  23008  dfef2  23025  basellem2  23080  basellem4  23082  basellem5  23083  basellem6  23084  basellem8  23086  isppw2  23114  vmappw  23115  sqf11  23138  vma1  23165  1sgm2ppw  23200  chtublem  23211  fsumvma2  23214  vmasum  23216  dchrelbas4  23243  dchrzrhcl  23245  dchrfi  23255  dchrhash  23271  pcbcctr  23276  bclbnd  23280  bposlem1  23284  lgsval4a  23318  lgsdchrval  23347  lgsdchr  23348  rplogsumlem2  23395  dchrisumlem2  23400  ostth2lem1  23528  ostth2lem3  23545  ostth3  23548  cusgrasize2inds  24150  cyclnspth  24304  clwwlkel  24466  clwwlkf  24467  clwwlkf1  24469  wwlksubclwwlk  24477  clwwisshclwwlem  24479  clwlkf1clwwlklem  24522  rusgra0edg  24628  clwlknclwlkdifnum  24634  clwwlkextfrlem1  24750  numclwwlkqhash  24774  numclwwlk2lem1  24776  numclwlk2lem2f  24777  numclwlk2lem2f1o  24779  gxcl  24940  ipval2  25290  ipasslem3  25421  ipasslem4  25422  ishashinf  27271  nn0min  27276  esumcst  27708  eulerpartlemb  27944  fibp1  27977  ballotlem1  28062  subfacp1lem6  28266  subfaclim  28269  subfacval3  28270  snmlff  28411  fallfacfwd  28732  0fallfac  28733  0risefac  28734  faclim2  28747  dvdspw  28749  opnmbllem0  29625  nn0prpwlem  29715  nnubfi  29844  nninfnub  29845  geomcau  29853  heiborlem5  29912  heiborlem6  29913  heiborlem7  29914  heiborlem8  29915  bfplem1  29919  irrapxlem2  30361  pellexlem1  30367  pellexlem5  30371  pellqrex  30417  monotoddzzfi  30480  expmordi  30485  rpexpmord  30486  jm2.17c  30502  acongeq  30523  jm2.18  30534  jm2.23  30542  jm2.26lem3  30547  jm3.1  30566  expdiophlem1  30567  idomrootle  30757  idomodle  30758  hashgcdlem  30762  phisum  30764  proot1ex  30766  nnne1ge2  31058  stoweidlem3  31303  stoweidlem7  31307  stoweidlem34  31334  wallispilem4  31368  wallispilem5  31369  wallispi2lem1  31371  wallispi2lem2  31372  stirlinglem2  31375  stirlinglem3  31376  stirlinglem4  31377  stirlinglem5  31378  stirlinglem7  31380  stirlinglem11  31384  stirlinglem14  31387  stirlinglem15  31388  stirlingr  31390  fourierdlem15  31422  fourierdlem21  31428  fourierdlem22  31429  fourierdlem92  31499  fouriersw  31532  ztprmneprm  32000  altgsumbc  32005  altgsumbcALT  32006