Theorem nnnn0d 10746

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

Syntax hints:   -> wi 4   e. wcel 1758   NNcn 10432   NN0cn0 10689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3078  df-un 3440  df-in 3442  df-ss 3449  df-n0 10690

This theorem is referenced by:  nnzd  10856  expgt1  12018  expaddzlem  12023  expaddz  12024  expmulz  12026  expmulnbnd  12112  facwordi  12181  faclbnd  12182  facavg  12193  bcm1k  12207  wrdeqs1cat  12486  isercolllem2  13260  bcxmas  13415  climcndslem1  13429  climcndslem2  13430  climcnds  13431  geo2sum  13450  mertenslem1  13461  eftabs  13478  efcllem  13480  eftlub  13510  eirrlem  13603  rpnnen2lem9  13622  rpnnen2lem11  13624  dvdsfac  13705  bitsfzo  13748  bitsfi  13750  sadcaddlem  13770  smumullem  13805  gcdcl  13818  mulgcd  13847  rplpwr  13857  rppwr  13858  nprmdvds1  13914  isprm5  13915  rpexp  13923  zsqrelqelz  13953  dfphi2  13966  phiprmpw  13968  eulerthlem2  13974  eulerth  13975  fermltl  13976  odzcllem  13981  odzdvds  13984  odzphi  13985  pythagtriplem6  14005  pythagtriplem7  14006  pcprmpw2  14065  pcprod  14074  pcfac  14078  pcbc  14079  expnprm  14081  pockthlem  14083  pockthg  14084  prmunb  14092  prmreclem2  14095  prmreclem3  14096  prmreclem4  14097  prmreclem5  14098  prmreclem6  14099  mul4sqlem  14131  4sqlem11  14133  4sqlem17  14139  vdwlem1  14159  vdwlem5  14163  vdwlem6  14164  vdwlem8  14166  vdwlem9  14167  vdwlem11  14169  vdwlem12  14170  vdwnnlem3  14175  ramz2  14202  ramub1lem1  14204  ramub1lem2  14205  ramub1  14206  2expltfac  14236  psgnunilem3  16120  mndodconglem  16164  gexcl3  16206  pgpfi1  16214  sylow1lem1  16217  gexexlem  16454  prmcyg  16490  gsumval3OLD  16502  gsumval3  16505  ablfacrplem  16687  ablfacrp  16688  ablfacrp2  16689  ablfac1eu  16695  srgbinomlem3  16762  srgbinomlem4  16763  ovoliunlem1  21116  mbfi1fseqlem1  21325  mbfi1fseqlem3  21327  mbfi1fseqlem5  21329  itg2cnlem2  21372  dvply1  21882  aalioulem2  21931  aalioulem5  21934  aaliou3lem1  21940  aaliou3lem2  21941  aaliou3lem8  21943  aaliou3lem6  21946  taylthlem1  21970  taylthlem2  21971  pserdvlem2  22025  cxpeq  22327  wilthlem1  22538  ftalem1  22542  ftalem2  22543  ftalem4  22545  ftalem5  22546  basellem2  22551  basellem3  22552  basellem4  22553  basellem5  22554  isppw2  22585  dvdsmulf1o  22666  sgmmul  22672  chpchtsum  22690  logfacubnd  22692  mersenne  22698  perfect1  22699  perfectlem1  22700  perfectlem2  22701  perfect  22702  dchrelbas3  22709  dchrelbasd  22710  dchrzrh1  22715  dchrzrhmul  22717  dchrmulcl  22720  dchrn0  22721  dchrfi  22726  dchrghm  22727  dchrabs  22731  dchrinv  22732  dchrptlem1  22735  dchrptlem2  22736  dchrptlem3  22737  dchrpt  22738  dchrsum2  22739  sum2dchr  22745  pcbcctr  22747  bcmono  22748  bclbnd  22751  bposlem1  22755  bposlem3  22757  bposlem5  22759  bposlem6  22760  lgslem1  22767  lgslem4  22770  lgsval2lem  22777  lgsvalmod  22786  lgsmod  22792  lgsdirprm  22800  lgsne0  22804  lgsqrlem1  22812  lgsqrlem2  22813  lgsqrlem3  22814  lgsqrlem4  22815  lgseisenlem1  22820  lgseisenlem2  22821  lgseisenlem3  22822  lgseisenlem4  22823  lgseisen  22824  lgsquadlem2  22826  lgsquadlem3  22827  m1lgs  22833  2sqlem3  22837  2sqblem  22848  chebbnd1lem1  22850  chebbnd1lem3  22852  rplogsumlem2  22866  rpvmasumlem  22868  dchrisumlem1  22870  dchrisumlem2  22871  dchrmusum2  22875  dchrvmasumlem3  22880  dchrisum0ff  22888  dchrisum0flblem1  22889  rpvmasum2  22893  dchrisum0re  22894  dchrisum0lem2a  22898  dirith  22910  mudivsum  22911  pntpbnd1a  22966  pntlemq  22982  pntlemr  22983  pntlemj  22984  ostth2lem2  23015  ostth2lem3  23016  ostth2  23018  dipcl  24261  dipcn  24269  sspival  24287  bcm1n  26223  isarchi2  26346  submarchi  26347  nexple  26592  oddpwdc  26880  eulerpartlemsv2  26884  eulerpartlemsf  26885  eulerpartlems  26886  eulerpartlemv  26890  eulerpartlemb  26894  plymulx0  27091  signsvtn0  27114  dmgmdivn0  27157  lgamgulmlem5  27162  lgamcvg2  27184  subfacp1lem1  27210  subfacp1lem6  27216  subfaclim  27219  erdszelem8  27229  erdszelem10  27231  cvmliftlem10  27326  prodmolem3  27589  prodmolem2a  27590  faclim2  27697  bpolydiflem  28340  nninfnub  28794  bfplem1  28868  3rexfrabdioph  29282  4rexfrabdioph  29283  6rexfrabdioph  29284  7rexfrabdioph  29285  irrapxlem5  29314  pellexlem2  29318  pellexlem6  29322  pell14qrgt0  29347  pell1qrge1  29358  pellfundgt1  29371  ltrmxnn0  29439  jm2.26lem3  29497  jm2.27a  29501  jm2.27c  29503  rmxdiophlem  29511  jm3.1lem1  29513  jm3.1lem2  29514  jm3.1lem3  29515  jm3.1  29516  dgrsub2  29638  mpaaeu  29654  idomsubgmo  29710  dvsinexp  29934  itgsinexplem1  29941  stoweidlem1  29943  stoweidlem17  29959  stoweidlem25  29967  stoweidlem34  29976  stoweidlem38  29980  stoweidlem40  29982  stoweidlem42  29984  stoweidlem45  29987  stirlinglem4  30019  stirlinglem5  30020  stirlinglem10  30025  stirlinglem13  30028  nn0ge2m1nn0  30332  eluzge2nn0  30339  erclwwlktr0  30626  hashecclwwlkn1  30655  usghashecclwwlk  30656  hashclwwlkn  30657  clwwlkndivn  30658  clwlkfclwwlk  30664  numclwwlk3  30849  numclwwlk6  30853  numclwwlk7  30854  chfacfscmulgsum  31331  chfacfpmmulgsum  31335  cpmadugsumlemF  31347