MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnnn0 Unicode version

Theorem nnnn0 9988
Description: A natural number is a nonnegative integer. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nnnn0  |-  ( A  e.  NN  ->  A  e.  NN0 )

Proof of Theorem nnnn0
StepHypRef Expression
1 nnssnn0 9984 . 2  |-  NN  C_  NN0
21sseli 3189 1  |-  ( A  e.  NN  ->  A  e.  NN0 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   NNcn 9762   NN0cn0 9981
This theorem is referenced by:  nnnn0i  9989  elnnnn0b  10024  elnnnn0c  10025  elz2  10056  nn0ind-raph  10128  zindd  10129  quoremnn0ALT  10977  modmulnn  11004  expneg  11127  expcllem  11130  expcl2lem  11131  expeq0  11148  mulexpz  11158  expnlbnd  11247  expmulnbnd  11249  digit2  11250  digit1  11251  facdiv  11316  faclbnd  11319  faclbnd3  11321  faclbnd4lem3  11324  faclbnd4lem4  11325  faclbnd5  11327  faclbnd6  11328  bcval5  11346  iswrdi  11433  wrdeqcats1  11490  absexpz  11806  isercoll  12157  summolem3  12203  summolem2a  12204  climcndslem2  12325  climcnds  12326  harmonic  12333  arisum  12334  expcnv  12338  geo2sum  12345  geo2lim  12347  geoisum1  12351  geoisum1c  12352  0.999...  12353  mertenslem2  12357  ef0lem  12376  ege2le3  12387  efaddlem  12390  efexp  12397  xpnnenOLD  12504  rpnnen2lem2  12510  rpnnen2lem4  12512  ruclem12  12535  divalg2  12620  ndvdssub  12622  gcddiv  12744  gcdmultiple  12745  gcdmultiplez  12746  rpmulgcd  12750  rplpwr  12751  dvdssqlem  12754  eucalgf  12769  1nprm  12779  isprm6  12804  isprm5  12807  prmdvdsexp  12809  phicl2  12852  phibndlem  12854  phiprmpw  12860  crt  12862  eulerthlem2  12866  pythagtriplem10  12889  pythagtriplem6  12890  pythagtriplem7  12891  pythagtriplem12  12895  pythagtriplem14  12897  pclem  12907  pcexp  12928  pcid  12941  pcprod  12959  pcbc  12964  prmpwdvds  12967  infpnlem1  12973  infpnlem2  12974  prmunb  12977  prmreclem6  12984  1arith  12990  vdwapf  13035  0hashbc  13070  ram0  13085  ghmmulg  14711  odmodnn0  14871  dfod2  14893  submod  14896  prmirredlem  16462  prmirred  16464  znf1o  16521  znhash  16528  znfi  16529  znfld  16530  znidomb  16531  znunithash  16534  znrrg  16535  tgpmulg  17792  ovollb2lem  18863  ovoliunlem1  18877  ovoliunlem3  18879  uniioombllem3  18956  uniioombllem4  18957  opnmbllem  18972  mbfi1fseqlem1  19086  mbfi1fseqlem3  19088  mbfi1fseqlem4  19089  mbfi1fseqlem5  19090  mbfi1fseqlem6  19091  dvexp  19318  dvexp3  19341  plyco  19639  dgrcolem1  19670  plydivex  19693  aaliou3lem2  19739  aaliou3lem3  19740  aaliou3lem5  19743  aaliou3lem6  19744  aaliou3lem7  19745  aaliou3lem9  19746  radcnvlem2  19806  dvradcnv  19813  pserdv2  19822  abelthlem6  19828  abelthlem9  19832  logtayllem  20022  logtayl  20023  logtaylsum  20024  logtayl2  20025  cxproot  20053  root1id  20110  atantayl  20249  atantayl2  20250  leibpilem2  20253  leibpi  20254  birthdaylem2  20263  birthdaylem3  20264  dfef2  20281  basellem2  20335  basellem4  20337  basellem5  20338  basellem6  20339  basellem8  20341  isppw2  20369  vmappw  20370  sqf11  20393  vma1  20420  1sgm2ppw  20455  chtublem  20466  fsumvma2  20469  vmasum  20471  dchrelbas4  20498  dchrzrhcl  20500  dchrfi  20510  dchrhash  20526  pcbcctr  20531  bclbnd  20535  bposlem1  20539  lgsval4a  20573  lgsdchrval  20602  lgsdchr  20603  rplogsumlem2  20650  dchrisumlem2  20655  ostth2lem1  20783  ostth2lem3  20800  ostth3  20803  gxcl  20948  ipval2  21296  ipasslem3  21427  ipasslem4  21428  ballotlem1  23061  ishashinf  23404  esumcst  23451  subfacp1lem6  23731  subfaclim  23734  subfacval3  23735  snmlff  23927  dvdspw  24174  cntrset  25705  nn0prpwlem  26341  nnubfi  26563  nninfnub  26564  geomcau  26578  heiborlem5  26642  heiborlem6  26643  heiborlem7  26644  heiborlem8  26645  bfplem1  26649  irrapxlem2  27011  pellexlem1  27017  pellexlem5  27021  pellqrex  27067  monotoddzzfi  27130  expmordi  27135  rpexpmord  27136  jm2.17c  27152  acongeq  27173  jm2.18  27184  jm2.23  27192  jm2.26lem3  27197  jm3.1  27216  expdiophlem1  27217  idomrootle  27614  idomodle  27615  hashgcdlem  27619  phisum  27621  proot1ex  27623  stoweidlem1  27853  stoweidlem3  27855  stoweidlem7  27859  stoweidlem17  27869  stoweidlem25  27877  stoweidlem34  27886  stoweidlem38  27890  stoweidlem40  27892  stoweidlem42  27894  stoweidlem45  27897  wallispilem4  27920  wallispilem5  27921  wallispi2lem1  27923  wallispi2lem2  27924  stirlinglem2  27927  stirlinglem3  27928  stirlinglem4  27929  stirlinglem5  27930  stirlinglem7  27932  stirlinglem11  27936  stirlinglem14  27939  stirlinglem15  27940  stirlingr  27942  cyclnspth  28376
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-in 3172  df-ss 3179  df-n0 9982
  Copyright terms: Public domain W3C validator