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

Theorem nnnn0d 10624
Description: A positive integer 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 10570 . 2  |-  NN  C_  NN0
2 nnnn0d.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3342 1  |-  ( ph  ->  A  e.  NN0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   NNcn 10310   NN0cn0 10567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-un 3321  df-in 3323  df-ss 3330  df-n0 10568
This theorem is referenced by:  nnzd  10734  expgt1  11886  expaddzlem  11891  expaddz  11892  expmulz  11894  expmulnbnd  11980  facwordi  12049  faclbnd  12050  facavg  12061  bcm1k  12075  wrdeqs1cat  12353  isercolllem2  13127  bcxmas  13281  climcndslem1  13295  climcndslem2  13296  climcnds  13297  geo2sum  13316  mertenslem1  13327  eftabs  13344  efcllem  13346  eftlub  13376  eirrlem  13469  rpnnen2lem9  13488  rpnnen2lem11  13490  dvdsfac  13571  bitsfzo  13614  bitsfi  13616  sadcaddlem  13636  smumullem  13671  gcdcl  13684  mulgcd  13713  rplpwr  13723  rppwr  13724  nprmdvds1  13780  isprm5  13781  rpexp  13789  zsqrelqelz  13819  dfphi2  13832  phiprmpw  13834  eulerthlem2  13840  eulerth  13841  fermltl  13842  odzcllem  13847  odzdvds  13850  odzphi  13851  pythagtriplem6  13871  pythagtriplem7  13872  pcprmpw2  13931  pcprod  13940  pcfac  13944  pcbc  13945  expnprm  13947  pockthlem  13949  pockthg  13950  prmunb  13958  prmreclem2  13961  prmreclem3  13962  prmreclem4  13963  prmreclem5  13964  prmreclem6  13965  mul4sqlem  13997  4sqlem11  13999  4sqlem17  14005  vdwlem1  14025  vdwlem5  14029  vdwlem6  14030  vdwlem8  14032  vdwlem9  14033  vdwlem11  14035  vdwlem12  14036  vdwnnlem3  14041  ramz2  14068  ramub1lem1  14070  ramub1lem2  14071  ramub1  14072  2expltfac  14102  psgnunilem3  15982  mndodconglem  16024  gexcl3  16066  pgpfi1  16074  sylow1lem1  16077  gexexlem  16314  prmcyg  16350  gsumval3OLD  16362  gsumval3  16365  ablfacrplem  16540  ablfacrp  16541  ablfacrp2  16542  ablfac1eu  16548  ovoliunlem1  20827  mbfi1fseqlem1  21035  mbfi1fseqlem3  21037  mbfi1fseqlem5  21039  itg2cnlem2  21082  dvply1  21635  aalioulem2  21684  aalioulem5  21687  aaliou3lem1  21693  aaliou3lem2  21694  aaliou3lem8  21696  aaliou3lem6  21699  taylthlem1  21723  taylthlem2  21724  pserdvlem2  21778  cxpeq  22080  wilthlem1  22291  ftalem1  22295  ftalem2  22296  ftalem4  22298  ftalem5  22299  basellem2  22304  basellem3  22305  basellem4  22306  basellem5  22307  isppw2  22338  dvdsmulf1o  22419  sgmmul  22425  chpchtsum  22443  logfacubnd  22445  mersenne  22451  perfect1  22452  perfectlem1  22453  perfectlem2  22454  perfect  22455  dchrelbas3  22462  dchrelbasd  22463  dchrzrh1  22468  dchrzrhmul  22470  dchrmulcl  22473  dchrn0  22474  dchrfi  22479  dchrghm  22480  dchrabs  22484  dchrinv  22485  dchrptlem1  22488  dchrptlem2  22489  dchrptlem3  22490  dchrpt  22491  dchrsum2  22492  sum2dchr  22498  pcbcctr  22500  bcmono  22501  bclbnd  22504  bposlem1  22508  bposlem3  22510  bposlem5  22512  bposlem6  22513  lgslem1  22520  lgslem4  22523  lgsval2lem  22530  lgsvalmod  22539  lgsmod  22545  lgsdirprm  22553  lgsne0  22557  lgsqrlem1  22565  lgsqrlem2  22566  lgsqrlem3  22567  lgsqrlem4  22568  lgseisenlem1  22573  lgseisenlem2  22574  lgseisenlem3  22575  lgseisenlem4  22576  lgseisen  22577  lgsquadlem2  22579  lgsquadlem3  22580  m1lgs  22586  2sqlem3  22590  2sqblem  22601  chebbnd1lem1  22603  chebbnd1lem3  22605  rplogsumlem2  22619  rpvmasumlem  22621  dchrisumlem1  22623  dchrisumlem2  22624  dchrmusum2  22628  dchrvmasumlem3  22633  dchrisum0ff  22641  dchrisum0flblem1  22642  rpvmasum2  22646  dchrisum0re  22647  dchrisum0lem2a  22651  dirith  22663  mudivsum  22664  pntpbnd1a  22719  pntlemq  22735  pntlemr  22736  pntlemj  22737  ostth2lem2  22768  ostth2lem3  22769  ostth2  22771  dipcl  23933  dipcn  23941  sspival  23959  bcm1n  25902  isarchi2  26026  submarchi  26027  nexple  26302  oddpwdc  26585  eulerpartlemsv2  26589  eulerpartlemsf  26590  eulerpartlems  26591  eulerpartlemv  26595  eulerpartlemb  26599  plymulx0  26796  signsvtn0  26819  dmgmdivn0  26862  lgamgulmlem5  26867  lgamcvg2  26889  subfacp1lem1  26915  subfacp1lem6  26921  subfaclim  26924  erdszelem8  26934  erdszelem10  26936  cvmliftlem10  27031  prodmolem3  27293  prodmolem2a  27294  faclim2  27401  bpolydiflem  28044  nninfnub  28491  bfplem1  28565  3rexfrabdioph  28980  4rexfrabdioph  28981  6rexfrabdioph  28982  7rexfrabdioph  28983  irrapxlem5  29012  pellexlem2  29016  pellexlem6  29020  pell14qrgt0  29045  pell1qrge1  29056  pellfundgt1  29069  ltrmxnn0  29137  jm2.26lem3  29195  jm2.27a  29199  jm2.27c  29201  rmxdiophlem  29209  jm3.1lem1  29211  jm3.1lem2  29212  jm3.1lem3  29213  jm3.1  29214  dgrsub2  29336  mpaaeu  29352  idomsubgmo  29408  dvsinexp  29633  itgsinexplem1  29640  stoweidlem1  29642  stoweidlem17  29658  stoweidlem25  29666  stoweidlem34  29675  stoweidlem38  29679  stoweidlem40  29681  stoweidlem42  29683  stoweidlem45  29686  stirlinglem4  29718  stirlinglem5  29719  stirlinglem10  29724  stirlinglem13  29727  nn0ge2m1nn0  30031  eluzge2nn0  30038  erclwwlktr0  30325  hashecclwwlkn1  30354  usghashecclwwlk  30355  hashclwwlkn  30356  clwwlkndivn  30357  clwlkfclwwlk  30363  numclwwlk3  30548  numclwwlk6  30552  numclwwlk7  30553
  Copyright terms: Public domain W3C validator