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

Theorem nnnn0 9972
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 9968 . 2  |-  NN  C_  NN0
21sseli 3176 1  |-  ( A  e.  NN  ->  A  e.  NN0 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   NNcn 9746   NN0cn0 9965
This theorem is referenced by:  nnnn0i  9973  elnnnn0b  10008  elnnnn0c  10009  elz2  10040  nn0ind-raph  10112  zindd  10113  quoremnn0ALT  10961  modmulnn  10988  expneg  11111  expcllem  11114  expcl2lem  11115  expeq0  11132  mulexpz  11142  expnlbnd  11231  expmulnbnd  11233  digit2  11234  digit1  11235  facdiv  11300  faclbnd  11303  faclbnd3  11305  faclbnd4lem3  11308  faclbnd4lem4  11309  faclbnd5  11311  faclbnd6  11312  bcval5  11330  iswrdi  11417  wrdeqcats1  11474  absexpz  11790  isercoll  12141  summolem3  12187  summolem2a  12188  climcndslem2  12309  climcnds  12310  harmonic  12317  arisum  12318  expcnv  12322  geo2sum  12329  geo2lim  12331  geoisum1  12335  geoisum1c  12336  0.999...  12337  mertenslem2  12341  ef0lem  12360  ege2le3  12371  efaddlem  12374  efexp  12381  xpnnenOLD  12488  rpnnen2lem2  12494  rpnnen2lem4  12496  ruclem12  12519  divalg2  12604  ndvdssub  12606  gcddiv  12728  gcdmultiple  12729  gcdmultiplez  12730  rpmulgcd  12734  rplpwr  12735  dvdssqlem  12738  eucalgf  12753  1nprm  12763  isprm6  12788  isprm5  12791  prmdvdsexp  12793  phicl2  12836  phibndlem  12838  phiprmpw  12844  crt  12846  eulerthlem2  12850  pythagtriplem10  12873  pythagtriplem6  12874  pythagtriplem7  12875  pythagtriplem12  12879  pythagtriplem14  12881  pclem  12891  pcexp  12912  pcid  12925  pcprod  12943  pcbc  12948  prmpwdvds  12951  infpnlem1  12957  infpnlem2  12958  prmunb  12961  prmreclem6  12968  1arith  12974  vdwapf  13019  0hashbc  13054  ram0  13069  ghmmulg  14695  odmodnn0  14855  dfod2  14877  submod  14880  prmirredlem  16446  prmirred  16448  znf1o  16505  znhash  16512  znfi  16513  znfld  16514  znidomb  16515  znunithash  16518  znrrg  16519  tgpmulg  17776  ovollb2lem  18847  ovoliunlem1  18861  ovoliunlem3  18863  uniioombllem3  18940  uniioombllem4  18941  opnmbllem  18956  mbfi1fseqlem1  19070  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  mbfi1fseqlem6  19075  dvexp  19302  dvexp3  19325  plyco  19623  dgrcolem1  19654  plydivex  19677  aaliou3lem2  19723  aaliou3lem3  19724  aaliou3lem5  19727  aaliou3lem6  19728  aaliou3lem7  19729  aaliou3lem9  19730  radcnvlem2  19790  dvradcnv  19797  pserdv2  19806  abelthlem6  19812  abelthlem9  19816  logtayllem  20006  logtayl  20007  logtaylsum  20008  logtayl2  20009  cxproot  20037  root1id  20094  atantayl  20233  atantayl2  20234  leibpilem2  20237  leibpi  20238  birthdaylem2  20247  birthdaylem3  20248  dfef2  20265  basellem2  20319  basellem4  20321  basellem5  20322  basellem6  20323  basellem8  20325  isppw2  20353  vmappw  20354  sqf11  20377  vma1  20404  1sgm2ppw  20439  chtublem  20450  fsumvma2  20453  vmasum  20455  dchrelbas4  20482  dchrzrhcl  20484  dchrfi  20494  dchrhash  20510  pcbcctr  20515  bclbnd  20519  bposlem1  20523  lgsval4a  20557  lgsdchrval  20586  lgsdchr  20587  rplogsumlem2  20634  dchrisumlem2  20639  ostth2lem1  20767  ostth2lem3  20784  ostth3  20787  gxcl  20932  ipval2  21280  ipasslem3  21411  ipasslem4  21412  ballotlem1  23045  ishashinf  23389  esumcst  23436  subfacp1lem6  23716  subfaclim  23719  subfacval3  23720  snmlff  23912  dvdspw  24103  cntrset  25602  nn0prpwlem  26238  nnubfi  26460  nninfnub  26461  geomcau  26475  heiborlem5  26539  heiborlem6  26540  heiborlem7  26541  heiborlem8  26542  bfplem1  26546  irrapxlem2  26908  pellexlem1  26914  pellexlem5  26918  pellqrex  26964  monotoddzzfi  27027  expmordi  27032  rpexpmord  27033  jm2.17c  27049  acongeq  27070  jm2.18  27081  jm2.23  27089  jm2.26lem3  27094  jm3.1  27113  expdiophlem1  27114  idomrootle  27511  idomodle  27512  hashgcdlem  27516  phisum  27518  proot1ex  27520  stoweidlem1  27750  stoweidlem3  27752  stoweidlem7  27756  stoweidlem17  27766  stoweidlem25  27774  stoweidlem34  27783  stoweidlem38  27787  stoweidlem40  27789  stoweidlem42  27791  stoweidlem45  27794  wallispilem4  27817  wallispilem5  27818  wallispi2lem1  27820  wallispi2lem2  27821  stirlinglem2  27824  stirlinglem3  27825  stirlinglem4  27826  stirlinglem5  27827  stirlinglem7  27829  stirlinglem11  27833  stirlinglem14  27836  stirlinglem15  27837  stirlingr  27839
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-ss 3166  df-n0 9966
  Copyright terms: Public domain W3C validator