Theorem nnnn0d 10895

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 10841	. 2 |- NN C_ NN0
2		nnnn0d.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sseldi 3442	1 |- ( ph -> A e. NN0 )

Syntax hints:   -> wi 4   e. wcel 1844   NNcn 10578   NN0cn0 10838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382

This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-v 3063  df-un 3421  df-in 3423  df-ss 3430  df-n0 10839

This theorem is referenced by:  nn0ge2m1nn0  10905  nnzd  11009  eluzge2nn0  11168  expgt1  12250  expaddzlem  12255  expaddz  12256  expmulz  12258  expmulnbnd  12344  facwordi  12413  faclbnd  12414  facavg  12425  bcm1k  12439  wrdeqs1cat  12758  cshwcsh2id  12854  relexpsucnnr  13009  isercolllem2  13639  bcxmas  13800  climcndslem1  13814  climcndslem2  13815  climcnds  13816  geo2sum  13836  mertenslem1  13847  prodmolem3  13894  prodmolem2a  13895  bpolydiflem  14001  eftabs  14022  efcllem  14024  eftlub  14055  eirrlem  14148  rpnnen2lem9  14167  rpnnen2lem11  14169  dvdsfac  14252  bitsfzo  14296  bitsfi  14298  sadcaddlem  14318  smumullem  14353  gcdcl  14366  mulgcd  14395  rplpwr  14405  rppwr  14406  nprmdvds1  14463  rpexp  14472  zsqrtelqelz  14502  phiprmpw  14517  eulerthlem2  14523  eulerth  14524  fermltl  14525  odzcllem  14530  odzdvds  14533  odzphi  14534  pythagtriplem6  14556  pythagtriplem7  14557  pcprmpw2  14616  pcprod  14625  pcfac  14629  pcbc  14630  expnprm  14632  pockthlem  14634  pockthg  14635  prmunb  14643  prmreclem2  14646  prmreclem3  14647  prmreclem4  14648  prmreclem5  14649  prmreclem6  14650  mul4sqlem  14682  4sqlem11  14684  4sqlem17  14690  vdwlem1  14710  vdwlem5  14714  vdwlem6  14715  vdwlem8  14717  vdwlem9  14718  vdwlem11  14720  vdwlem12  14721  vdwnnlem3  14726  ramz2  14753  ramub1lem1  14755  ramub1lem2  14756  ramub1  14757  2expltfac  14788  psgnunilem3  16847  mndodconglem  16891  gexcl3  16933  pgpfi1  16941  sylow1lem1  16944  gexexlem  17184  prmcyg  17222  gsumval3OLD  17234  gsumval3  17237  ablfacrplem  17438  ablfacrp  17439  ablfacrp2  17440  ablfac1eu  17446  srgbinomlem3  17515  srgbinomlem4  17516  chfacfscmulgsum  19655  chfacfpmmulgsum  19659  cpmadugsumlemF  19671  ovoliunlem1  22207  mbfi1fseqlem1  22416  mbfi1fseqlem3  22418  mbfi1fseqlem5  22420  itg2cnlem2  22463  dvply1  22974  aalioulem2  23023  aalioulem5  23026  aaliou3lem1  23032  aaliou3lem2  23033  aaliou3lem8  23035  aaliou3lem6  23038  taylthlem1  23062  taylthlem2  23063  pserdvlem2  23117  cxpeq  23429  dmgmdivn0  23685  lgamgulmlem5  23690  lgamcvg2  23712  wilthlem1  23725  ftalem1  23729  ftalem2  23730  ftalem4  23732  ftalem5  23733  basellem2  23738  basellem3  23739  basellem4  23740  basellem5  23741  isppw2  23772  dvdsmulf1o  23853  sgmmul  23859  chpchtsum  23877  logfacubnd  23879  mersenne  23885  perfect1  23886  perfectlem1  23887  perfectlem2  23888  perfect  23889  dchrelbas3  23896  dchrelbasd  23897  dchrzrh1  23902  dchrzrhmul  23904  dchrmulcl  23907  dchrn0  23908  dchrfi  23913  dchrghm  23914  dchrabs  23918  dchrinv  23919  dchrptlem1  23922  dchrptlem2  23923  dchrptlem3  23924  dchrpt  23925  dchrsum2  23926  sum2dchr  23932  pcbcctr  23934  bcmono  23935  bclbnd  23938  bposlem1  23942  bposlem3  23944  bposlem5  23946  bposlem6  23947  lgslem1  23954  lgslem4  23957  lgsval2lem  23964  lgsvalmod  23973  lgsmod  23979  lgsdirprm  23987  lgsne0  23991  lgsqrlem1  23999  lgsqrlem2  24000  lgsqrlem3  24001  lgsqrlem4  24002  lgseisenlem1  24007  lgseisenlem2  24008  lgseisenlem3  24009  lgseisenlem4  24010  lgseisen  24011  lgsquadlem2  24013  lgsquadlem3  24014  m1lgs  24020  2sqlem3  24024  2sqblem  24035  chebbnd1lem1  24037  chebbnd1lem3  24039  rplogsumlem2  24053  rpvmasumlem  24055  dchrisumlem1  24057  dchrisumlem2  24058  dchrmusum2  24062  dchrvmasumlem3  24067  dchrisum0ff  24075  dchrisum0flblem1  24076  rpvmasum2  24080  dchrisum0re  24081  dchrisum0lem2a  24085  dirith  24097  mudivsum  24098  pntpbnd1a  24153  pntlemq  24169  pntlemr  24170  pntlemj  24171  ostth2lem2  24202  ostth2lem3  24203  ostth2  24205  hashecclwwlkn1  25263  usghashecclwwlk  25264  hashclwwlkn  25265  clwwlkndivn  25266  clwlkfclwwlk  25273  numclwwlk3  25538  numclwwlk6  25542  numclwwlk7  25543  dipcl  26052  dipcn  26060  sspival  26078  bcm1n  28061  isarchi2  28194  submarchi  28195  nexple  28470  oddpwdc  28812  eulerpartlemsv2  28816  eulerpartlemsf  28817  eulerpartlems  28818  eulerpartlemv  28822  eulerpartlemb  28826  plymulx0  29023  signsvtn0  29046  subfacp1lem1  29489  subfacp1lem6  29495  subfaclim  29498  erdszelem8  29508  erdszelem10  29510  cvmliftlem10  29604  faclim2  29970  nninfnub  31539  bfplem1  31613  3rexfrabdioph  35105  4rexfrabdioph  35106  6rexfrabdioph  35107  7rexfrabdioph  35108  irrapxlem5  35136  pellexlem2  35140  pellexlem6  35144  pell14qrgt0  35169  pell1qrge1  35180  pellfundgt1  35193  ltrmxnn0  35261  jm2.26lem3  35318  jm2.27a  35322  jm2.27c  35324  rmxdiophlem  35332  jm3.1lem1  35334  jm3.1lem2  35335  jm3.1lem3  35336  jm3.1  35337  dgrsub2  35461  mpaaeu  35476  idomsubgmo  35532  relexpxpmin  35709  lcmcl  36068  nzprmdif  36085  binomcxplemwb  36114  fperiodmul  36886  fsumnncl  36953  dvsinexp  37086  dvxpaek  37118  itgsinexplem1  37133  stoweidlem1  37164  stoweidlem17  37180  stoweidlem25  37188  stoweidlem34  37197  stoweidlem38  37201  stoweidlem40  37203  stoweidlem42  37205  stoweidlem45  37208  stirlinglem4  37240  stirlinglem5  37241  stirlinglem10  37246  stirlinglem13  37249  dirkertrigeq  37264  fourierdlem21  37291  fourierdlem25  37295  fourierdlem48  37318  fourierdlem54  37324  fourierdlem64  37334  fourierdlem65  37335  fourierdlem73  37343  fourierdlem81  37351  fourierdlem83  37353  fourierdlem92  37362  fourierdlem103  37373  fourierdlem104  37374  fourierdlem112  37382  fourierdlem113  37383  etransclem1  37399  etransclem4  37402  etransclem8  37406  etransclem15  37413  etransclem17  37415  etransclem18  37416  etransclem19  37417  etransclem20  37418  etransclem21  37419  etransclem22  37420  etransclem23  37421  etransclem24  37422  etransclem25  37423  etransclem27  37425  etransclem32  37430  etransclem35  37433  etransclem41  37439  etransclem44  37442  etransclem46  37444  iccpartigtl  37703  iccpartgt  37707  iccpartgel  37709  iccelpart  37713  perfectALTVlem1  37809  perfectALTVlem2  37810  perfectALTV  37811  proththdlem  37872  proththd  37873  logbpw2m1  38711  nnpw2blenfzo  38725  nnolog2flm1  38734  dignn0fr  38745  nn0sumshdiglemA  38763  nn0sumshdiglemB  38764