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

Theorem nnnn0d 10107
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 10057 . 2  |-  NN  C_  NN0
2 nnnn0d.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3254 1  |-  ( ph  ->  A  e.  NN0 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710   NNcn 9833   NN0cn0 10054
This theorem is referenced by:  nnzd  10205  expgt1  11230  expaddzlem  11235  expaddz  11236  expmulz  11238  expmulnbnd  11323  facwordi  11392  faclbnd  11393  facavg  11404  bcm1k  11417  wrdeqs1cat  11565  isercolllem2  12229  bcxmas  12385  climcndslem1  12399  climcndslem2  12400  climcnds  12401  geo2sum  12420  mertenslem1  12431  eftabs  12448  efcllem  12450  eftlub  12480  eirrlem  12573  rpnnen2lem9  12592  rpnnen2lem11  12594  dvdsfac  12674  bitsfzo  12717  bitsfi  12719  sadcaddlem  12739  smumullem  12774  gcdcl  12787  mulgcd  12816  rplpwr  12826  rppwr  12827  nprmdvds1  12881  isprm5  12882  rpexp  12890  zsqrelqelz  12920  dfphi2  12933  phiprmpw  12935  eulerthlem2  12941  eulerth  12942  fermltl  12943  odzcllem  12948  odzdvds  12951  odzphi  12952  pythagtriplem6  12965  pythagtriplem7  12966  pcprmpw2  13025  pcprod  13034  pcfac  13038  pcbc  13039  expnprm  13041  pockthlem  13043  pockthg  13044  prmunb  13052  prmreclem2  13055  prmreclem3  13056  prmreclem4  13057  prmreclem5  13058  prmreclem6  13059  mul4sqlem  13091  4sqlem11  13093  4sqlem17  13099  vdwlem1  13119  vdwlem5  13123  vdwlem6  13124  vdwlem8  13126  vdwlem9  13127  vdwlem11  13129  vdwlem12  13130  vdwnnlem3  13135  ramz2  13162  ramub1lem1  13164  ramub1lem2  13165  ramub1  13166  2expltfac  13196  mndodconglem  14949  gexcl3  14991  pgpfi1  14999  sylow1lem1  15002  gexexlem  15237  prmcyg  15273  gsumval3  15284  ablfacrplem  15393  ablfacrp  15394  ablfacrp2  15395  ablfac1eu  15401  ovoliunlem1  18959  mbfi1fseqlem1  19168  mbfi1fseqlem3  19170  mbfi1fseqlem5  19172  itg2cnlem2  19215  dvply1  19762  aalioulem2  19811  aalioulem5  19814  aaliou3lem1  19820  aaliou3lem2  19821  aaliou3lem8  19823  aaliou3lem6  19826  taylthlem1  19850  taylthlem2  19851  pserdvlem2  19905  cxpeq  20202  wilthlem1  20412  ftalem1  20416  ftalem2  20417  ftalem4  20419  ftalem5  20420  basellem2  20425  basellem3  20426  basellem4  20427  basellem5  20428  isppw2  20459  dvdsmulf1o  20540  sgmmul  20546  chpchtsum  20564  logfacubnd  20566  mersenne  20572  perfect1  20573  perfectlem1  20574  perfectlem2  20575  perfect  20576  dchrelbas3  20583  dchrelbasd  20584  dchrzrh1  20589  dchrzrhmul  20591  dchrmulcl  20594  dchrn0  20595  dchrfi  20600  dchrghm  20601  dchrabs  20605  dchrinv  20606  dchrptlem1  20609  dchrptlem2  20610  dchrptlem3  20611  dchrpt  20612  dchrsum2  20613  sum2dchr  20619  pcbcctr  20621  bcmono  20622  bclbnd  20625  bposlem1  20629  bposlem3  20631  bposlem5  20633  bposlem6  20634  lgslem1  20641  lgslem4  20644  lgsval2lem  20651  lgsvalmod  20660  lgsmod  20666  lgsdirprm  20674  lgsne0  20678  lgsqrlem1  20686  lgsqrlem2  20687  lgsqrlem3  20688  lgsqrlem4  20689  lgseisenlem1  20694  lgseisenlem2  20695  lgseisenlem3  20696  lgseisenlem4  20697  lgseisen  20698  lgsquadlem2  20700  lgsquadlem3  20701  m1lgs  20707  2sqlem3  20711  2sqblem  20722  chebbnd1lem1  20724  chebbnd1lem3  20726  rplogsumlem2  20740  rpvmasumlem  20742  dchrisumlem1  20744  dchrisumlem2  20745  dchrmusum2  20749  dchrvmasumlem3  20754  dchrisum0ff  20762  dchrisum0flblem1  20763  rpvmasum2  20767  dchrisum0re  20768  dchrisum0lem2a  20772  dirith  20784  mudivsum  20785  pntpbnd1a  20840  pntlemq  20856  pntlemr  20857  pntlemj  20858  ostth2lem2  20889  ostth2lem3  20890  ostth2  20892  dipcl  21396  dipcn  21404  sspival  21422  bcm1n  23350  dmgmdivn0  24061  lgamgulmlem5  24066  lgamcvg2  24088  subfacp1lem1  24114  subfacp1lem6  24120  subfaclim  24123  erdszelem8  24133  erdszelem10  24135  cvmliftlem10  24229  prodmolem3  24560  prodmolem2a  24561  gammacvglem1  24651  gammacvglem2  24652  faclim2  24659  bpolydiflem  25348  nninfnub  25785  bfplem1  25869  3rexfrabdioph  26201  4rexfrabdioph  26202  6rexfrabdioph  26203  7rexfrabdioph  26204  irrapxlem5  26234  pellexlem2  26238  pellexlem6  26242  pell14qrgt0  26267  pell1qrge1  26278  pellfundgt1  26291  ltrmxnn0  26359  jm2.26lem3  26417  jm2.27a  26421  jm2.27c  26423  rmxdiophlem  26431  jm3.1lem1  26433  jm3.1lem2  26434  jm3.1lem3  26435  dgrsub2  26662  mpaaeu  26678  psgnunilem3  26742  idomsubgmo  26837  dvsinexp  27063  itgsinexplem1  27071  stirlinglem4  27149  stirlinglem5  27150  stirlinglem10  27155  stirlinglem13  27158
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-un 3233  df-in 3235  df-ss 3242  df-n0 10055
  Copyright terms: Public domain W3C validator