Theorem nnnn0 10698

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

Syntax hints:   -> wi 4   e. wcel 1758   NNcn 10434   NN0cn0 10691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-un 3442  df-in 3444  df-ss 3451  df-n0 10692

This theorem is referenced by:  nnnn0i  10699  elnnnn0b  10736  elnnnn0c  10737  elz2  10775  nn0ind-raph  10854  zindd  10855  fzo1fzo0n0  11706  ubmelfzo  11721  fzo0sn0fzo1  11735  quoremnn0ALT  11814  modmulnn  11843  expneg  11991  expcllem  11994  expcl2lem  11995  expeq0  12012  mulexpz  12022  expnlbnd  12112  expmulnbnd  12114  digit2  12115  digit1  12116  facdiv  12181  faclbnd  12184  faclbnd3  12186  faclbnd4lem3  12189  faclbnd4lem4  12190  faclbnd5  12192  faclbnd6  12193  bcval5  12212  iswrdi  12358  swrdn0  12443  swrdtrcfv  12456  swrdccatwrd  12481  wrdeqcats1  12487  repswfsts  12538  repswlsw  12539  repswcshw  12565  absexpz  12913  isercoll  13264  summolem3  13310  summolem2a  13311  climcndslem2  13432  climcnds  13433  harmonic  13440  arisum  13441  expcnv  13445  geo2sum  13452  geo2lim  13454  geoisum1  13458  geoisum1c  13459  0.999...  13460  mertenslem2  13464  ef0lem  13483  ege2le3  13494  efaddlem  13497  efexp  13504  xpnnenOLD  13611  rpnnen2lem2  13617  rpnnen2lem4  13619  ruclem12  13642  divalg2  13728  ndvdssub  13730  gcddiv  13852  gcdmultiple  13853  gcdmultiplez  13854  rpmulgcd  13858  rplpwr  13859  dvdssqlem  13862  eucalgf  13877  1nprm  13887  isprm6  13914  isprm5  13917  prmdvdsexp  13919  phicl2  13962  phibndlem  13964  phiprmpw  13970  crt  13972  eulerthlem2  13976  pythagtriplem10  14006  pythagtriplem6  14007  pythagtriplem7  14008  pythagtriplem12  14012  pythagtriplem14  14014  pclem  14024  pcexp  14045  pcid  14058  pcprod  14076  pcbc  14081  prmpwdvds  14084  infpnlem1  14090  infpnlem2  14091  prmunb  14094  prmreclem6  14101  1arith  14107  vdwapf  14152  0hashbc  14187  ram0  14202  cshwrepswhash1  14248  ghmmulg  15879  odmodnn0  16165  dfod2  16187  submod  16190  prmirredlem  18043  prmirred  18045  prmirredlemOLD  18046  prmirredOLD  18048  znf1o  18110  znhash  18117  znfi  18118  znfld  18119  znidomb  18120  znunithash  18123  znrrg  18124  tgpmulg  19797  ovollb2lem  21104  ovoliunlem1  21118  ovoliunlem3  21120  uniioombllem3  21199  uniioombllem4  21200  opnmbllem  21215  mbfi1fseqlem1  21327  mbfi1fseqlem3  21329  mbfi1fseqlem4  21330  mbfi1fseqlem5  21331  mbfi1fseqlem6  21332  dvexp  21561  dvexp3  21584  plyco  21843  dgrcolem1  21874  plydivex  21897  aaliou3lem2  21943  aaliou3lem3  21944  aaliou3lem5  21947  aaliou3lem6  21948  aaliou3lem7  21949  aaliou3lem9  21950  radcnvlem2  22013  dvradcnv  22020  pserdv2  22029  abelthlem6  22035  abelthlem9  22039  logtayllem  22238  logtayl  22239  logtaylsum  22240  logtayl2  22241  cxproot  22269  root1id  22326  atantayl  22466  atantayl2  22467  leibpilem2  22470  leibpi  22471  birthdaylem2  22480  birthdaylem3  22481  dfef2  22498  basellem2  22553  basellem4  22555  basellem5  22556  basellem6  22557  basellem8  22559  isppw2  22587  vmappw  22588  sqf11  22611  vma1  22638  1sgm2ppw  22673  chtublem  22684  fsumvma2  22687  vmasum  22689  dchrelbas4  22716  dchrzrhcl  22718  dchrfi  22728  dchrhash  22744  pcbcctr  22749  bclbnd  22753  bposlem1  22757  lgsval4a  22791  lgsdchrval  22820  lgsdchr  22821  rplogsumlem2  22868  dchrisumlem2  22873  ostth2lem1  23001  ostth2lem3  23018  ostth3  23021  cusgrasize2inds  23538  cyclnspth  23670  gxcl  23905  ipval2  24255  ipasslem3  24386  ipasslem4  24387  ishashinf  26231  nn0min  26236  esumcst  26660  eulerpartlemb  26896  fibp1  26929  ballotlem1  27014  subfacp1lem6  27218  subfaclim  27221  subfacval3  27222  snmlff  27363  fallfacfwd  27684  0fallfac  27685  0risefac  27686  faclim2  27699  dvdspw  27701  opnmbllem0  28576  nn0prpwlem  28666  nnubfi  28795  nninfnub  28796  geomcau  28804  heiborlem5  28863  heiborlem6  28864  heiborlem7  28865  heiborlem8  28866  bfplem1  28870  irrapxlem2  29313  pellexlem1  29319  pellexlem5  29323  pellqrex  29369  monotoddzzfi  29432  expmordi  29437  rpexpmord  29438  jm2.17c  29454  acongeq  29475  jm2.18  29486  jm2.23  29494  jm2.26lem3  29499  jm3.1  29518  expdiophlem1  29519  idomrootle  29709  idomodle  29710  hashgcdlem  29714  phisum  29716  proot1ex  29718  stoweidlem3  29947  stoweidlem7  29951  stoweidlem34  29978  wallispilem4  30012  wallispilem5  30013  wallispi2lem1  30015  wallispi2lem2  30016  stirlinglem2  30019  stirlinglem3  30020  stirlinglem4  30021  stirlinglem5  30022  stirlinglem7  30024  stirlinglem11  30028  stirlinglem14  30031  stirlinglem15  30032  stirlingr  30034  clwwlkel  30604  clwwlkf  30605  clwwlkf1  30607  wwlksubclwwlk  30615  clwwisshclwwlem  30619  clwlkf1clwwlklem  30671  rusgra0edg  30722  clwlknclwlkdifnum  30728  clwwlkextfrlem1  30818  numclwwlkqhash  30842  numclwwlk2lem1  30844  numclwlk2lem2f  30845  numclwlk2lem2f1o  30847  ztprmneprm  30888  altgsumbc  30898  altgsumbcALT  30899  cply1coe0  31004  cply1coe0bi  31005  cply1mul  31006  cpmatmcllem  31208  m2cpm  31231  m2pminv2lem  31239  fvmptnn04ifa  31337  chfacfisf  31341  chfacfisfcpmat  31342  chfacffsupp  31343  chfacfscmul0  31345  chfacfscmulfsupp  31346  chfacfscmulgsum  31347  chfacfpmmul0  31349  chfacfpmmulfsupp  31350  chfacfpmmulgsum  31351  chfacfpmmulgsum2  31352  cayhamlem1  31353  cpmadugsumlemF  31363