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

Theorem nnnn0 10229
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 10225 . 2  |-  NN  C_  NN0
21sseli 3345 1  |-  ( A  e.  NN  ->  A  e.  NN0 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   NNcn 10001   NN0cn0 10222
This theorem is referenced by:  nnnn0i  10230  elnnnn0b  10265  elnnnn0c  10266  elz2  10299  nn0ind-raph  10371  zindd  10372  quoremnn0ALT  11239  modmulnn  11266  expneg  11390  expcllem  11393  expcl2lem  11394  expeq0  11411  mulexpz  11421  expnlbnd  11510  expmulnbnd  11512  digit2  11513  digit1  11514  facdiv  11579  faclbnd  11582  faclbnd3  11584  faclbnd4lem3  11587  faclbnd4lem4  11588  faclbnd5  11590  faclbnd6  11591  bcval5  11610  iswrdi  11732  wrdeqcats1  11789  absexpz  12111  isercoll  12462  summolem3  12509  summolem2a  12510  climcndslem2  12631  climcnds  12632  harmonic  12639  arisum  12640  expcnv  12644  geo2sum  12651  geo2lim  12653  geoisum1  12657  geoisum1c  12658  0.999...  12659  mertenslem2  12663  ef0lem  12682  ege2le3  12693  efaddlem  12696  efexp  12703  xpnnenOLD  12810  rpnnen2lem2  12816  rpnnen2lem4  12818  ruclem12  12841  divalg2  12926  ndvdssub  12928  gcddiv  13050  gcdmultiple  13051  gcdmultiplez  13052  rpmulgcd  13056  rplpwr  13057  dvdssqlem  13060  eucalgf  13075  1nprm  13085  isprm6  13110  isprm5  13113  prmdvdsexp  13115  phicl2  13158  phibndlem  13160  phiprmpw  13166  crt  13168  eulerthlem2  13172  pythagtriplem10  13195  pythagtriplem6  13196  pythagtriplem7  13197  pythagtriplem12  13201  pythagtriplem14  13203  pclem  13213  pcexp  13234  pcid  13247  pcprod  13265  pcbc  13270  prmpwdvds  13273  infpnlem1  13279  infpnlem2  13280  prmunb  13283  prmreclem6  13290  1arith  13296  vdwapf  13341  0hashbc  13376  ram0  13391  ghmmulg  15019  odmodnn0  15179  dfod2  15201  submod  15204  prmirredlem  16774  prmirred  16776  znf1o  16833  znhash  16840  znfi  16841  znfld  16842  znidomb  16843  znunithash  16846  znrrg  16847  tgpmulg  18124  ovollb2lem  19385  ovoliunlem1  19399  ovoliunlem3  19401  uniioombllem3  19478  uniioombllem4  19479  opnmbllem  19494  mbfi1fseqlem1  19608  mbfi1fseqlem3  19610  mbfi1fseqlem4  19611  mbfi1fseqlem5  19612  mbfi1fseqlem6  19613  dvexp  19840  dvexp3  19863  plyco  20161  dgrcolem1  20192  plydivex  20215  aaliou3lem2  20261  aaliou3lem3  20262  aaliou3lem5  20265  aaliou3lem6  20266  aaliou3lem7  20267  aaliou3lem9  20268  radcnvlem2  20331  dvradcnv  20338  pserdv2  20347  abelthlem6  20353  abelthlem9  20357  logtayllem  20551  logtayl  20552  logtaylsum  20553  logtayl2  20554  cxproot  20582  root1id  20639  atantayl  20778  atantayl2  20779  leibpilem2  20782  leibpi  20783  birthdaylem2  20792  birthdaylem3  20793  dfef2  20810  basellem2  20865  basellem4  20867  basellem5  20868  basellem6  20869  basellem8  20871  isppw2  20899  vmappw  20900  sqf11  20923  vma1  20950  1sgm2ppw  20985  chtublem  20996  fsumvma2  20999  vmasum  21001  dchrelbas4  21028  dchrzrhcl  21030  dchrfi  21040  dchrhash  21056  pcbcctr  21061  bclbnd  21065  bposlem1  21069  lgsval4a  21103  lgsdchrval  21132  lgsdchr  21133  rplogsumlem2  21180  dchrisumlem2  21185  ostth2lem1  21313  ostth2lem3  21330  ostth3  21333  cusgrasize2inds  21487  cyclnspth  21619  gxcl  21854  ipval2  22204  ipasslem3  22335  ipasslem4  22336  ishashinf  24160  esumcst  24456  ballotlem1  24745  subfacp1lem6  24872  subfaclim  24875  subfacval3  24876  snmlff  25017  fallfacfwd  25353  0fallfac  25354  0risefac  25355  faclim2  25368  dvdspw  25370  opnmbllem0  26243  nn0prpwlem  26326  nnubfi  26455  nninfnub  26456  geomcau  26466  heiborlem5  26525  heiborlem6  26526  heiborlem7  26527  heiborlem8  26528  bfplem1  26532  irrapxlem2  26887  pellexlem1  26893  pellexlem5  26897  pellqrex  26943  monotoddzzfi  27006  expmordi  27011  rpexpmord  27012  jm2.17c  27028  acongeq  27049  jm2.18  27060  jm2.23  27068  jm2.26lem3  27073  jm3.1  27092  expdiophlem1  27093  idomrootle  27489  idomodle  27490  hashgcdlem  27494  phisum  27496  proot1ex  27498  stoweidlem3  27729  stoweidlem7  27733  stoweidlem34  27760  wallispilem4  27794  wallispilem5  27795  wallispi2lem1  27797  wallispi2lem2  27798  stirlinglem2  27801  stirlinglem3  27802  stirlinglem4  27803  stirlinglem5  27804  stirlinglem7  27806  stirlinglem11  27810  stirlinglem14  27813  stirlinglem15  27814  stirlingr  27816  fzo0sn0fzo1  28126  fzo1fzo0n0  28129  swrdtrcfv  28195
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-v 2959  df-un 3326  df-in 3328  df-ss 3335  df-n0 10223
  Copyright terms: Public domain W3C validator