Theorem nnnn0d 10859

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

Syntax hints:   -> wi 4   e. wcel 1804   NNcn 10543   NN0cn0 10802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-in 3468  df-ss 3475  df-n0 10803

This theorem is referenced by:  nn0ge2m1nn0  10869  nnzd  10975  eluzge2nn0  11131  expgt1  12186  expaddzlem  12191  expaddz  12192  expmulz  12194  expmulnbnd  12280  facwordi  12349  faclbnd  12350  facavg  12361  bcm1k  12375  wrdeqs1cat  12682  cshwcsh2id  12778  isercolllem2  13470  bcxmas  13629  climcndslem1  13643  climcndslem2  13644  climcnds  13645  geo2sum  13664  mertenslem1  13675  prodmolem3  13722  prodmolem2a  13723  eftabs  13793  efcllem  13795  eftlub  13826  eirrlem  13919  rpnnen2lem9  13938  rpnnen2lem11  13940  dvdsfac  14023  bitsfzo  14067  bitsfi  14069  sadcaddlem  14089  smumullem  14124  gcdcl  14137  mulgcd  14166  rplpwr  14176  rppwr  14177  nprmdvds1  14234  rpexp  14243  zsqrtelqelz  14273  phiprmpw  14288  eulerthlem2  14294  eulerth  14295  fermltl  14296  odzcllem  14301  odzdvds  14304  odzphi  14305  pythagtriplem6  14327  pythagtriplem7  14328  pcprmpw2  14387  pcprod  14396  pcfac  14400  pcbc  14401  expnprm  14403  pockthlem  14405  pockthg  14406  prmunb  14414  prmreclem2  14417  prmreclem3  14418  prmreclem4  14419  prmreclem5  14420  prmreclem6  14421  mul4sqlem  14453  4sqlem11  14455  4sqlem17  14461  vdwlem1  14481  vdwlem5  14485  vdwlem6  14486  vdwlem8  14488  vdwlem9  14489  vdwlem11  14491  vdwlem12  14492  vdwnnlem3  14497  ramz2  14524  ramub1lem1  14526  ramub1lem2  14527  ramub1  14528  2expltfac  14559  psgnunilem3  16500  mndodconglem  16544  gexcl3  16586  pgpfi1  16594  sylow1lem1  16597  gexexlem  16837  prmcyg  16875  gsumval3OLD  16887  gsumval3  16890  ablfacrplem  17095  ablfacrp  17096  ablfacrp2  17097  ablfac1eu  17103  srgbinomlem3  17172  srgbinomlem4  17173  chfacfscmulgsum  19339  chfacfpmmulgsum  19343  cpmadugsumlemF  19355  ovoliunlem1  21891  mbfi1fseqlem1  22100  mbfi1fseqlem3  22102  mbfi1fseqlem5  22104  itg2cnlem2  22147  dvply1  22658  aalioulem2  22707  aalioulem5  22710  aaliou3lem1  22716  aaliou3lem2  22717  aaliou3lem8  22719  aaliou3lem6  22722  taylthlem1  22746  taylthlem2  22747  pserdvlem2  22801  cxpeq  23109  wilthlem1  23320  ftalem1  23324  ftalem2  23325  ftalem4  23327  ftalem5  23328  basellem2  23333  basellem3  23334  basellem4  23335  basellem5  23336  isppw2  23367  dvdsmulf1o  23448  sgmmul  23454  chpchtsum  23472  logfacubnd  23474  mersenne  23480  perfect1  23481  perfectlem1  23482  perfectlem2  23483  perfect  23484  dchrelbas3  23491  dchrelbasd  23492  dchrzrh1  23497  dchrzrhmul  23499  dchrmulcl  23502  dchrn0  23503  dchrfi  23508  dchrghm  23509  dchrabs  23513  dchrinv  23514  dchrptlem1  23517  dchrptlem2  23518  dchrptlem3  23519  dchrpt  23520  dchrsum2  23521  sum2dchr  23527  pcbcctr  23529  bcmono  23530  bclbnd  23533  bposlem1  23537  bposlem3  23539  bposlem5  23541  bposlem6  23542  lgslem1  23549  lgslem4  23552  lgsval2lem  23559  lgsvalmod  23568  lgsmod  23574  lgsdirprm  23582  lgsne0  23586  lgsqrlem1  23594  lgsqrlem2  23595  lgsqrlem3  23596  lgsqrlem4  23597  lgseisenlem1  23602  lgseisenlem2  23603  lgseisenlem3  23604  lgseisenlem4  23605  lgseisen  23606  lgsquadlem2  23608  lgsquadlem3  23609  m1lgs  23615  2sqlem3  23619  2sqblem  23630  chebbnd1lem1  23632  chebbnd1lem3  23634  rplogsumlem2  23648  rpvmasumlem  23650  dchrisumlem1  23652  dchrisumlem2  23653  dchrmusum2  23657  dchrvmasumlem3  23662  dchrisum0ff  23670  dchrisum0flblem1  23671  rpvmasum2  23675  dchrisum0re  23676  dchrisum0lem2a  23680  dirith  23692  mudivsum  23693  pntpbnd1a  23748  pntlemq  23764  pntlemr  23765  pntlemj  23766  ostth2lem2  23797  ostth2lem3  23798  ostth2  23800  hashecclwwlkn1  24812  usghashecclwwlk  24813  hashclwwlkn  24814  clwwlkndivn  24815  clwlkfclwwlk  24822  numclwwlk3  25087  numclwwlk6  25091  numclwwlk7  25092  dipcl  25603  dipcn  25611  sspival  25629  bcm1n  27578  isarchi2  27707  submarchi  27708  nexple  27983  oddpwdc  28271  eulerpartlemsv2  28275  eulerpartlemsf  28276  eulerpartlems  28277  eulerpartlemv  28281  eulerpartlemb  28285  plymulx0  28482  signsvtn0  28505  dmgmdivn0  28548  lgamgulmlem5  28553  lgamcvg2  28575  subfacp1lem1  28601  subfacp1lem6  28607  subfaclim  28610  erdszelem8  28620  erdszelem10  28622  cvmliftlem10  28717  faclim2  29149  bpolydiflem  29792  nninfnub  30220  bfplem1  30294  3rexfrabdioph  30706  4rexfrabdioph  30707  6rexfrabdioph  30708  7rexfrabdioph  30709  irrapxlem5  30738  pellexlem2  30742  pellexlem6  30746  pell14qrgt0  30771  pell1qrge1  30782  pellfundgt1  30795  ltrmxnn0  30863  jm2.26lem3  30919  jm2.27a  30923  jm2.27c  30925  rmxdiophlem  30933  jm3.1lem1  30935  jm3.1lem2  30936  jm3.1lem3  30937  jm3.1  30938  dgrsub2  31060  mpaaeu  31075  idomsubgmo  31131  lcmcl  31183  nzprmdif  31200  fperiodmul  31458  fsumnncl  31526  dvsinexp  31659  dvxpaek  31691  itgsinexplem1  31706  stoweidlem1  31737  stoweidlem17  31753  stoweidlem25  31761  stoweidlem34  31770  stoweidlem38  31774  stoweidlem40  31776  stoweidlem42  31778  stoweidlem45  31781  stirlinglem4  31813  stirlinglem5  31814  stirlinglem10  31819  stirlinglem13  31822  dirkertrigeq  31837  fourierdlem21  31864  fourierdlem25  31868  fourierdlem48  31891  fourierdlem54  31897  fourierdlem64  31907  fourierdlem65  31908  fourierdlem73  31916  fourierdlem81  31924  fourierdlem83  31926  fourierdlem92  31935  fourierdlem103  31946  fourierdlem104  31947  fourierdlem112  31955  fourierdlem113  31956  etransclem1  31972  etransclem4  31975  etransclem8  31979  etransclem15  31986  etransclem17  31988  etransclem18  31989  etransclem19  31990  etransclem20  31991  etransclem21  31992  etransclem22  31993  etransclem23  31994  etransclem24  31995  etransclem25  31996  etransclem27  31998  etransclem28  31999  etransclem32  32003  etransclem35  32006  etransclem41  32012  etransclem44  32015  etransclem46  32017