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

Theorem nnnn0d 10018
Description: A natural number is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nnnn0d.1  |-  ( ph  ->  A  e.  NN )
Assertion
Ref Expression
nnnn0d  |-  ( ph  ->  A  e.  NN0 )

Proof of Theorem nnnn0d
StepHypRef Expression
1 nnssnn0 9968 . 2  |-  NN  C_  NN0
2 nnnn0d.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3178 1  |-  ( ph  ->  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:  nnzd  10116  expgt1  11140  expaddzlem  11145  expaddz  11146  expmulz  11148  expmulnbnd  11233  facwordi  11302  faclbnd  11303  facavg  11314  bcm1k  11327  wrdeqs1cat  11475  isercolllem2  12139  bcxmas  12294  climcndslem1  12308  climcndslem2  12309  climcnds  12310  geo2sum  12329  mertenslem1  12340  eftabs  12357  efcllem  12359  eftlub  12389  eirrlem  12482  rpnnen2lem9  12501  rpnnen2lem11  12503  dvdsfac  12583  bitsfzo  12626  bitsfi  12628  sadcaddlem  12648  smumullem  12683  gcdcl  12696  mulgcd  12725  rplpwr  12735  rppwr  12736  nprmdvds1  12790  isprm5  12791  rpexp  12799  zsqrelqelz  12829  dfphi2  12842  phiprmpw  12844  eulerthlem2  12850  eulerth  12851  fermltl  12852  odzcllem  12857  odzdvds  12860  odzphi  12861  pythagtriplem6  12874  pythagtriplem7  12875  pcprmpw2  12934  pcprod  12943  pcfac  12947  pcbc  12948  expnprm  12950  pockthlem  12952  pockthg  12953  prmunb  12961  prmreclem2  12964  prmreclem3  12965  prmreclem4  12966  prmreclem5  12967  prmreclem6  12968  mul4sqlem  13000  4sqlem11  13002  4sqlem17  13008  vdwlem1  13028  vdwlem5  13032  vdwlem6  13033  vdwlem8  13035  vdwlem9  13036  vdwlem11  13038  vdwlem12  13039  vdwnnlem3  13044  ramz2  13071  ramub1lem1  13073  ramub1lem2  13074  ramub1  13075  2expltfac  13105  mndodconglem  14856  gexcl3  14898  pgpfi1  14906  sylow1lem1  14909  gexexlem  15144  prmcyg  15180  gsumval3  15191  ablfacrplem  15300  ablfacrp  15301  ablfacrp2  15302  ablfac1eu  15308  ovoliunlem1  18861  mbfi1fseqlem1  19070  mbfi1fseqlem3  19072  mbfi1fseqlem5  19074  itg2cnlem2  19117  dvply1  19664  aalioulem2  19713  aalioulem5  19716  aaliou3lem1  19722  aaliou3lem2  19723  aaliou3lem8  19725  aaliou3lem6  19728  taylthlem1  19752  taylthlem2  19753  pserdvlem2  19804  cxpeq  20097  wilthlem1  20306  ftalem1  20310  ftalem2  20311  ftalem4  20313  ftalem5  20314  basellem2  20319  basellem3  20320  basellem4  20321  basellem5  20322  isppw2  20353  dvdsmulf1o  20434  sgmmul  20440  chpchtsum  20458  logfacubnd  20460  mersenne  20466  perfect1  20467  perfectlem1  20468  perfectlem2  20469  perfect  20470  dchrelbas3  20477  dchrelbasd  20478  dchrzrh1  20483  dchrzrhmul  20485  dchrmulcl  20488  dchrn0  20489  dchrfi  20494  dchrghm  20495  dchrabs  20499  dchrinv  20500  dchrptlem1  20503  dchrptlem2  20504  dchrptlem3  20505  dchrpt  20506  dchrsum2  20507  sum2dchr  20513  pcbcctr  20515  bcmono  20516  bclbnd  20519  bposlem1  20523  bposlem3  20525  bposlem5  20527  bposlem6  20528  lgslem1  20535  lgslem4  20538  lgsval2lem  20545  lgsvalmod  20554  lgsmod  20560  lgsdirprm  20568  lgsne0  20572  lgsqrlem1  20580  lgsqrlem2  20581  lgsqrlem3  20582  lgsqrlem4  20583  lgseisenlem1  20588  lgseisenlem2  20589  lgseisenlem3  20590  lgseisenlem4  20591  lgseisen  20592  lgsquadlem2  20594  lgsquadlem3  20595  m1lgs  20601  2sqlem3  20605  2sqblem  20616  chebbnd1lem1  20618  chebbnd1lem3  20620  rplogsumlem2  20634  rpvmasumlem  20636  dchrisumlem1  20638  dchrisumlem2  20639  dchrmusum2  20643  dchrvmasumlem3  20648  dchrisum0ff  20656  dchrisum0flblem1  20657  rpvmasum2  20661  dchrisum0re  20662  dchrisum0lem2a  20666  dirith  20678  mudivsum  20679  pntpbnd1a  20734  pntlemq  20750  pntlemr  20751  pntlemj  20752  ostth2lem2  20783  ostth2lem3  20784  ostth2  20786  dipcl  21288  dipcn  21296  sspival  21314  bcm1n  23032  subfacp1lem1  23710  subfacp1lem6  23716  subfaclim  23719  erdszelem8  23729  erdszelem10  23731  cvmliftlem10  23825  bpolydiflem  24789  nninfnub  26461  bfplem1  26546  3rexfrabdioph  26878  4rexfrabdioph  26879  6rexfrabdioph  26880  7rexfrabdioph  26881  irrapxlem5  26911  pellexlem2  26915  pellexlem6  26919  pell14qrgt0  26944  pell1qrge1  26955  pellfundgt1  26968  ltrmxnn0  27036  jm2.26lem3  27094  jm2.27a  27098  jm2.27c  27100  rmxdiophlem  27108  jm3.1lem1  27110  jm3.1lem2  27111  jm3.1lem3  27112  dgrsub2  27339  mpaaeu  27355  psgnunilem3  27419  idomsubgmo  27514  dvsinexp  27740  itgsinexplem1  27748  stirlinglem4  27826  stirlinglem5  27827  stirlinglem10  27832  stirlinglem13  27835
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