Theorem nnnn0d 10852

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

Syntax hints:   -> wi 4   e. wcel 1767   NNcn 10536   NN0cn0 10795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-in 3483  df-ss 3490  df-n0 10796

This theorem is referenced by:  nn0ge2m1nn0  10862  nnzd  10965  eluzge2nn0  11121  expgt1  12172  expaddzlem  12177  expaddz  12178  expmulz  12180  expmulnbnd  12266  facwordi  12335  faclbnd  12336  facavg  12347  bcm1k  12361  wrdeqs1cat  12663  cshwcsh2id  12759  isercolllem2  13451  bcxmas  13610  climcndslem1  13624  climcndslem2  13625  climcnds  13626  geo2sum  13645  mertenslem1  13656  eftabs  13673  efcllem  13675  eftlub  13705  eirrlem  13798  rpnnen2lem9  13817  rpnnen2lem11  13819  dvdsfac  13900  bitsfzo  13944  bitsfi  13946  sadcaddlem  13966  smumullem  14001  gcdcl  14014  mulgcd  14043  rplpwr  14053  rppwr  14054  nprmdvds1  14111  isprm5  14112  rpexp  14120  zsqrtelqelz  14150  dfphi2  14163  phiprmpw  14165  eulerthlem2  14171  eulerth  14172  fermltl  14173  odzcllem  14178  odzdvds  14181  odzphi  14182  pythagtriplem6  14204  pythagtriplem7  14205  pcprmpw2  14264  pcprod  14273  pcfac  14277  pcbc  14278  expnprm  14280  pockthlem  14282  pockthg  14283  prmunb  14291  prmreclem2  14294  prmreclem3  14295  prmreclem4  14296  prmreclem5  14297  prmreclem6  14298  mul4sqlem  14330  4sqlem11  14332  4sqlem17  14338  vdwlem1  14358  vdwlem5  14362  vdwlem6  14363  vdwlem8  14365  vdwlem9  14366  vdwlem11  14368  vdwlem12  14369  vdwnnlem3  14374  ramz2  14401  ramub1lem1  14403  ramub1lem2  14404  ramub1  14405  2expltfac  14435  psgnunilem3  16327  mndodconglem  16371  gexcl3  16413  pgpfi1  16421  sylow1lem1  16424  gexexlem  16661  prmcyg  16699  gsumval3OLD  16711  gsumval3  16714  ablfacrplem  16918  ablfacrp  16919  ablfacrp2  16920  ablfac1eu  16926  srgbinomlem3  16995  srgbinomlem4  16996  chfacfscmulgsum  19156  chfacfpmmulgsum  19160  cpmadugsumlemF  19172  ovoliunlem1  21676  mbfi1fseqlem1  21885  mbfi1fseqlem3  21887  mbfi1fseqlem5  21889  itg2cnlem2  21932  dvply1  22442  aalioulem2  22491  aalioulem5  22494  aaliou3lem1  22500  aaliou3lem2  22501  aaliou3lem8  22503  aaliou3lem6  22506  taylthlem1  22530  taylthlem2  22531  pserdvlem2  22585  cxpeq  22887  wilthlem1  23098  ftalem1  23102  ftalem2  23103  ftalem4  23105  ftalem5  23106  basellem2  23111  basellem3  23112  basellem4  23113  basellem5  23114  isppw2  23145  dvdsmulf1o  23226  sgmmul  23232  chpchtsum  23250  logfacubnd  23252  mersenne  23258  perfect1  23259  perfectlem1  23260  perfectlem2  23261  perfect  23262  dchrelbas3  23269  dchrelbasd  23270  dchrzrh1  23275  dchrzrhmul  23277  dchrmulcl  23280  dchrn0  23281  dchrfi  23286  dchrghm  23287  dchrabs  23291  dchrinv  23292  dchrptlem1  23295  dchrptlem2  23296  dchrptlem3  23297  dchrpt  23298  dchrsum2  23299  sum2dchr  23305  pcbcctr  23307  bcmono  23308  bclbnd  23311  bposlem1  23315  bposlem3  23317  bposlem5  23319  bposlem6  23320  lgslem1  23327  lgslem4  23330  lgsval2lem  23337  lgsvalmod  23346  lgsmod  23352  lgsdirprm  23360  lgsne0  23364  lgsqrlem1  23372  lgsqrlem2  23373  lgsqrlem3  23374  lgsqrlem4  23375  lgseisenlem1  23380  lgseisenlem2  23381  lgseisenlem3  23382  lgseisenlem4  23383  lgseisen  23384  lgsquadlem2  23386  lgsquadlem3  23387  m1lgs  23393  2sqlem3  23397  2sqblem  23408  chebbnd1lem1  23410  chebbnd1lem3  23412  rplogsumlem2  23426  rpvmasumlem  23428  dchrisumlem1  23430  dchrisumlem2  23431  dchrmusum2  23435  dchrvmasumlem3  23440  dchrisum0ff  23448  dchrisum0flblem1  23449  rpvmasum2  23453  dchrisum0re  23454  dchrisum0lem2a  23458  dirith  23470  mudivsum  23471  pntpbnd1a  23526  pntlemq  23542  pntlemr  23543  pntlemj  23544  ostth2lem2  23575  ostth2lem3  23576  ostth2  23578  hashecclwwlkn1  24538  usghashecclwwlk  24539  hashclwwlkn  24540  clwwlkndivn  24541  clwlkfclwwlk  24548  numclwwlk3  24814  numclwwlk6  24818  numclwwlk7  24819  dipcl  25329  dipcn  25337  sspival  25355  bcm1n  27296  isarchi2  27419  submarchi  27420  nexple  27673  oddpwdc  27961  eulerpartlemsv2  27965  eulerpartlemsf  27966  eulerpartlems  27967  eulerpartlemv  27971  eulerpartlemb  27975  plymulx0  28172  signsvtn0  28195  dmgmdivn0  28238  lgamgulmlem5  28243  lgamcvg2  28265  subfacp1lem1  28291  subfacp1lem6  28297  subfaclim  28300  erdszelem8  28310  erdszelem10  28312  cvmliftlem10  28407  prodmolem3  28670  prodmolem2a  28671  faclim2  28778  bpolydiflem  29421  nninfnub  29875  bfplem1  29949  3rexfrabdioph  30362  4rexfrabdioph  30363  6rexfrabdioph  30364  7rexfrabdioph  30365  irrapxlem5  30394  pellexlem2  30398  pellexlem6  30402  pell14qrgt0  30427  pell1qrge1  30438  pellfundgt1  30451  ltrmxnn0  30519  jm2.26lem3  30575  jm2.27a  30579  jm2.27c  30581  rmxdiophlem  30589  jm3.1lem1  30591  jm3.1lem2  30592  jm3.1lem3  30593  jm3.1  30594  dgrsub2  30716  mpaaeu  30732  idomsubgmo  30788  lcmcl  30835  nzprmdif  30852  fperiodmul  31109  dvsinexp  31266  itgsinexplem1  31299  stoweidlem1  31329  stoweidlem17  31345  stoweidlem25  31353  stoweidlem34  31362  stoweidlem38  31366  stoweidlem40  31368  stoweidlem42  31370  stoweidlem45  31373  stirlinglem4  31405  stirlinglem5  31406  stirlinglem10  31411  stirlinglem13  31414  dirkertrigeq  31429  fourierdlem21  31456  fourierdlem25  31460  fourierdlem48  31483  fourierdlem54  31489  fourierdlem64  31499  fourierdlem65  31500  fourierdlem73  31508  fourierdlem81  31516  fourierdlem103  31538  fourierdlem104  31539  fourierdlem113  31548