Theorem nnnn0d 10925

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

Step	Hyp	Ref	Expression
1		nnssnn0 10872	. 2 |- NN C_ NN0
2		nnnn0d.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sseldi 3462	1 |- ( ph -> A e. NN0 )

Syntax hints:   -> wi 4   e. wcel 1868   NNcn 10609   NN0cn0 10869

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-v 3083  df-un 3441  df-in 3443  df-ss 3450  df-n0 10870

This theorem is referenced by:  nn0ge2m1nn0  10935  nnzd  11039  eluzge2nn0  11198  expgt1  12309  expaddzlem  12314  expaddz  12315  expmulz  12317  expmulnbnd  12403  facwordi  12473  faclbnd  12474  facavg  12485  bcm1k  12499  wrdeqs1cat  12819  cshwcsh2id  12915  relexpsucnnr  13074  isercolllem2  13714  bcxmas  13878  climcndslem1  13892  climcndslem2  13893  climcnds  13894  geo2sum  13914  mertenslem1  13925  prodmolem3  13972  prodmolem2a  13973  bpolydiflem  14092  eftabs  14115  efcllem  14117  eftlub  14148  eirrlem  14241  rpnnen2lem9  14260  rpnnen2lem11  14262  dvdsfac  14345  bitsfzo  14394  bitsfi  14396  sadcaddlem  14416  smumullem  14451  gcdcl  14465  mulgcd  14499  rplpwr  14509  rppwr  14510  lcmcl  14551  lcmgcdnn  14561  lcmfcl  14586  nprmdvds1  14635  rpexp  14657  zsqrtelqelz  14692  phiprmpw  14709  eulerthlem2  14715  eulerth  14716  fermltl  14717  odzcllem  14722  odzdvds  14725  odzphi  14726  odzcllemOLD  14728  odzdvdsOLD  14731  odzphiOLD  14732  pythagtriplem6  14756  pythagtriplem7  14757  pcprmpw2  14816  pcprod  14825  pcfac  14829  pcbc  14830  expnprm  14832  pockthlem  14834  pockthg  14835  prmunb  14843  prmreclem2  14846  prmreclem3  14847  prmreclem4  14848  prmreclem5  14849  prmreclem6  14850  mul4sqlem  14882  4sqlem11  14884  4sqlem17OLD  14890  4sqlem17  14896  vdwlem1  14916  vdwlem5  14920  vdwlem6  14921  vdwlem8  14923  vdwlem9  14924  vdwlem11  14926  vdwlem12  14927  vdwnnlem3  14932  ramz2  14967  ramub1lem1  14969  ramub1lem2  14970  ramub1  14971  prmgaplem3  15008  2expltfac  15048  psgnunilem3  17122  mndodconglem  17175  gexcl3  17224  pgpfi1  17232  sylow1lem1  17235  gexexlem  17475  prmcyg  17513  gsumval3  17526  ablfacrplem  17683  ablfacrp  17684  ablfacrp2  17685  ablfac1eu  17691  srgbinomlem3  17760  srgbinomlem4  17761  chfacfscmulgsum  19868  chfacfpmmulgsum  19872  cpmadugsumlemF  19884  ovoliunlem1  22439  mbfi1fseqlem1  22657  mbfi1fseqlem3  22659  mbfi1fseqlem5  22661  itg2cnlem2  22704  dvply1  23221  aalioulem2  23273  aalioulem5  23276  aaliou3lem1  23282  aaliou3lem2  23283  aaliou3lem8  23285  aaliou3lem6  23288  taylthlem1  23312  taylthlem2  23313  pserdvlem2  23367  cxpeq  23681  dmgmdivn0  23937  lgamgulmlem5  23942  lgamcvg2  23964  wilthlem1  23977  ftalem1  23981  ftalem2  23982  ftalem4  23984  ftalem5  23985  ftalem4OLD  23986  ftalem5OLD  23987  basellem2  23992  basellem3  23993  basellem4  23994  basellem5  23995  isppw2  24026  dvdsmulf1o  24107  sgmmul  24113  chpchtsum  24131  logfacubnd  24133  mersenne  24139  perfect1  24140  perfectlem1  24141  perfectlem2  24142  perfect  24143  dchrelbas3  24150  dchrelbasd  24151  dchrzrh1  24156  dchrzrhmul  24158  dchrmulcl  24161  dchrn0  24162  dchrfi  24167  dchrghm  24168  dchrabs  24172  dchrinv  24173  dchrptlem1  24176  dchrptlem2  24177  dchrptlem3  24178  dchrpt  24179  dchrsum2  24180  sum2dchr  24186  pcbcctr  24188  bcmono  24189  bclbnd  24192  bposlem1  24196  bposlem3  24198  bposlem5  24200  bposlem6  24201  lgslem1  24208  lgslem4  24211  lgsval2lem  24218  lgsvalmod  24227  lgsmod  24233  lgsdirprm  24241  lgsne0  24245  lgsqrlem1  24253  lgsqrlem2  24254  lgsqrlem3  24255  lgsqrlem4  24256  lgseisenlem1  24261  lgseisenlem2  24262  lgseisenlem3  24263  lgseisenlem4  24264  lgseisen  24265  lgsquadlem2  24267  lgsquadlem3  24268  m1lgs  24274  2sqlem3  24278  2sqblem  24289  chebbnd1lem1  24291  chebbnd1lem3  24293  rplogsumlem2  24307  rpvmasumlem  24309  dchrisumlem1  24311  dchrisumlem2  24312  dchrmusum2  24316  dchrvmasumlem3  24321  dchrisum0ff  24329  dchrisum0flblem1  24330  rpvmasum2  24334  dchrisum0re  24335  dchrisum0lem2a  24339  dirith  24351  mudivsum  24352  pntpbnd1a  24407  pntlemq  24423  pntlemr  24424  pntlemj  24425  ostth2lem2  24456  ostth2lem3  24457  ostth2  24459  hashecclwwlkn1  25545  usghashecclwwlk  25546  hashclwwlkn  25547  clwwlkndivn  25548  clwlkfclwwlk  25555  numclwwlk3  25820  numclwwlk6  25824  numclwwlk7  25825  dipcl  26334  dipcn  26342  sspival  26360  bcm1n  28362  isarchi2  28494  submarchi  28495  psgnfzto1st  28611  submateqlem1  28626  madjusmdetlem2  28647  madjusmdetlem4  28649  mdetlap  28651  nexple  28824  oddpwdc  29180  eulerpartlemsv2  29184  eulerpartlemsf  29185  eulerpartlems  29186  eulerpartlemv  29190  eulerpartlemb  29194  plymulx0  29429  signsvtn0  29452  subfacp1lem1  29895  subfacp1lem6  29901  subfaclim  29904  erdszelem8  29914  erdszelem10  29916  cvmliftlem10  30010  faclim2  30376  poimirlem7  31858  poimirlem17  31868  poimirlem18  31869  poimirlem20  31871  poimirlem21  31872  poimirlem22  31873  poimirlem25  31876  poimirlem26  31877  poimirlem27  31878  poimirlem28  31879  poimirlem32  31883  nninfnub  31991  bfplem1  32065  3rexfrabdioph  35556  4rexfrabdioph  35557  6rexfrabdioph  35558  7rexfrabdioph  35559  irrapxlem5  35587  pellexlem2  35591  pellexlem6  35595  pell14qrgt0  35622  pell1qrge1  35633  pellfundgt1  35648  ltrmxnn0  35716  jm2.26lem3  35773  jm2.27a  35777  jm2.27c  35779  rmxdiophlem  35787  jm3.1lem1  35789  jm3.1lem2  35790  jm3.1lem3  35791  jm3.1  35792  dgrsub2  35911  mpaaeu  35933  idomsubgmo  35989  relexpxpmin  36166  nzprmdif  36523  binomcxplemwb  36552  fperiodmul  37361  fsumnncl  37470  dvsinexp  37597  dvxpaek  37632  itgsinexplem1  37647  stoweidlem1  37678  stoweidlem17  37694  stoweidlem25  37702  stoweidlem34  37712  stoweidlem38  37716  stoweidlem40  37718  stoweidlem42  37720  stoweidlem45  37723  stirlinglem4  37756  stirlinglem5  37757  stirlinglem10  37762  stirlinglem13  37765  dirkertrigeq  37780  fourierdlem21  37807  fourierdlem25  37811  fourierdlem48  37835  fourierdlem54  37841  fourierdlem64  37851  fourierdlem65  37852  fourierdlem73  37860  fourierdlem81  37868  fourierdlem83  37870  fourierdlem92  37879  fourierdlem103  37890  fourierdlem104  37891  fourierdlem112  37899  fourierdlem113  37900  etransclem1  37917  etransclem4  37920  etransclem8  37924  etransclem15  37931  etransclem17  37933  etransclem18  37934  etransclem19  37935  etransclem20  37936  etransclem21  37937  etransclem22  37938  etransclem23  37939  etransclem24  37940  etransclem25  37941  etransclem27  37943  etransclem32  37948  etransclem35  37951  etransclem41  37957  etransclem44  37960  etransclem46  37962  iccpartigtl  38446  iccpartgt  38450  iccpartgel  38452  iccelpart  38456  perfectALTVlem1  38552  perfectALTVlem2  38553  perfectALTV  38554  proththdlem  38622  proththd  38623  logbpw2m1  39566  nnpw2blenfzo  39580  nnolog2flm1  39589  dignn0fr  39600  nn0sumshdiglemA  39618  nn0sumshdiglemB  39619