Theorem nnnn0d 10959

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 10906	. 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 1898   NNcn 10642   NN0cn0 10903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-un 3421  df-in 3423  df-ss 3430  df-n0 10904

This theorem is referenced by:  nn0ge2m1nn0  10969  nnzd  11073  eluzge2nn0  11232  expgt1  12348  expaddzlem  12353  expaddz  12354  expmulz  12356  expmulnbnd  12442  facwordi  12512  faclbnd  12513  facavg  12524  bcm1k  12538  wrdeqs1cat  12874  cshwcsh2id  12970  relexpsucnnr  13143  isercolllem2  13784  bcxmas  13948  climcndslem1  13962  climcndslem2  13963  climcnds  13964  geo2sum  13984  mertenslem1  13995  prodmolem3  14042  prodmolem2a  14043  bpolydiflem  14162  eftabs  14185  efcllem  14187  eftlub  14218  eirrlem  14311  rpnnen2lem9  14330  rpnnen2lem11  14332  dvdsfac  14415  bitsfzo  14464  bitsfi  14466  sadcaddlem  14486  smumullem  14521  gcdcl  14535  mulgcd  14569  rplpwr  14579  rppwr  14580  lcmcl  14621  lcmgcdnn  14631  lcmfcl  14656  nprmdvds1  14705  rpexp  14727  zsqrtelqelz  14762  phiprmpw  14779  eulerthlem2  14785  eulerth  14786  fermltl  14787  odzcllem  14792  odzdvds  14795  odzphi  14796  odzcllemOLD  14798  odzdvdsOLD  14801  odzphiOLD  14802  pythagtriplem6  14826  pythagtriplem7  14827  pcprmpw2  14886  pcprod  14895  pcfac  14899  pcbc  14900  expnprm  14902  pockthlem  14904  pockthg  14905  prmunb  14913  prmreclem2  14916  prmreclem3  14917  prmreclem4  14918  prmreclem5  14919  prmreclem6  14920  mul4sqlem  14952  4sqlem11  14954  4sqlem17OLD  14960  4sqlem17  14966  vdwlem1  14986  vdwlem5  14990  vdwlem6  14991  vdwlem8  14993  vdwlem9  14994  vdwlem11  14996  vdwlem12  14997  vdwnnlem3  15002  ramz2  15037  ramub1lem1  15039  ramub1lem2  15040  ramub1  15041  prmgaplem3  15078  2expltfac  15118  psgnunilem3  17192  mndodconglem  17245  gexcl3  17294  pgpfi1  17302  sylow1lem1  17305  gexexlem  17545  prmcyg  17583  gsumval3  17596  ablfacrplem  17753  ablfacrp  17754  ablfacrp2  17755  ablfac1eu  17761  srgbinomlem3  17830  srgbinomlem4  17831  chfacfscmulgsum  19939  chfacfpmmulgsum  19943  cpmadugsumlemF  19955  ovoliunlem1  22510  mbfi1fseqlem1  22729  mbfi1fseqlem3  22731  mbfi1fseqlem5  22733  itg2cnlem2  22776  dvply1  23293  aalioulem2  23345  aalioulem5  23348  aaliou3lem1  23354  aaliou3lem2  23355  aaliou3lem8  23357  aaliou3lem6  23360  taylthlem1  23384  taylthlem2  23385  pserdvlem2  23439  cxpeq  23753  dmgmdivn0  24009  lgamgulmlem5  24014  lgamcvg2  24036  wilthlem1  24049  ftalem1  24053  ftalem2  24054  ftalem4  24056  ftalem5  24057  ftalem4OLD  24058  ftalem5OLD  24059  basellem2  24064  basellem3  24065  basellem4  24066  basellem5  24067  isppw2  24098  dvdsmulf1o  24179  sgmmul  24185  chpchtsum  24203  logfacubnd  24205  mersenne  24211  perfect1  24212  perfectlem1  24213  perfectlem2  24214  perfect  24215  dchrelbas3  24222  dchrelbasd  24223  dchrzrh1  24228  dchrzrhmul  24230  dchrmulcl  24233  dchrn0  24234  dchrfi  24239  dchrghm  24240  dchrabs  24244  dchrinv  24245  dchrptlem1  24248  dchrptlem2  24249  dchrptlem3  24250  dchrpt  24251  dchrsum2  24252  sum2dchr  24258  pcbcctr  24260  bcmono  24261  bclbnd  24264  bposlem1  24268  bposlem3  24270  bposlem5  24272  bposlem6  24273  lgslem1  24280  lgslem4  24283  lgsval2lem  24290  lgsvalmod  24299  lgsmod  24305  lgsdirprm  24313  lgsne0  24317  lgsqrlem1  24325  lgsqrlem2  24326  lgsqrlem3  24327  lgsqrlem4  24328  lgseisenlem1  24333  lgseisenlem2  24334  lgseisenlem3  24335  lgseisenlem4  24336  lgseisen  24337  lgsquadlem2  24339  lgsquadlem3  24340  m1lgs  24346  2sqlem3  24350  2sqblem  24361  chebbnd1lem1  24363  chebbnd1lem3  24365  rplogsumlem2  24379  rpvmasumlem  24381  dchrisumlem1  24383  dchrisumlem2  24384  dchrmusum2  24388  dchrvmasumlem3  24393  dchrisum0ff  24401  dchrisum0flblem1  24402  rpvmasum2  24406  dchrisum0re  24407  dchrisum0lem2a  24411  dirith  24423  mudivsum  24424  pntpbnd1a  24479  pntlemq  24495  pntlemr  24496  pntlemj  24497  ostth2lem2  24528  ostth2lem3  24529  ostth2  24531  hashecclwwlkn1  25618  usghashecclwwlk  25619  hashclwwlkn  25620  clwwlkndivn  25621  clwlkfclwwlk  25628  numclwwlk3  25893  numclwwlk6  25897  numclwwlk7  25898  dipcl  26407  dipcn  26415  sspival  26433  bcm1n  28423  isarchi2  28553  submarchi  28554  psgnfzto1st  28669  submateqlem1  28684  madjusmdetlem2  28705  madjusmdetlem4  28707  mdetlap  28709  nexple  28882  oddpwdc  29237  eulerpartlemsv2  29241  eulerpartlemsf  29242  eulerpartlems  29243  eulerpartlemv  29247  eulerpartlemb  29251  plymulx0  29486  signsvtn0  29509  subfacp1lem1  29952  subfacp1lem6  29958  subfaclim  29961  erdszelem8  29971  erdszelem10  29973  cvmliftlem10  30067  faclim2  30434  poimirlem7  31993  poimirlem17  32003  poimirlem18  32004  poimirlem20  32006  poimirlem21  32007  poimirlem22  32008  poimirlem25  32011  poimirlem26  32012  poimirlem27  32013  poimirlem28  32014  poimirlem32  32018  nninfnub  32126  bfplem1  32200  3rexfrabdioph  35686  4rexfrabdioph  35687  6rexfrabdioph  35688  7rexfrabdioph  35689  irrapxlem5  35716  pellexlem2  35720  pellexlem6  35724  pell14qrgt0  35751  pell1qrge1  35762  pellfundgt1  35777  ltrmxnn0  35845  jm2.26lem3  35902  jm2.27a  35906  jm2.27c  35908  rmxdiophlem  35916  jm3.1lem1  35918  jm3.1lem2  35919  jm3.1lem3  35920  jm3.1  35921  dgrsub2  36040  mpaaeu  36062  idomsubgmo  36118  relexpxpmin  36355  nzprmdif  36713  binomcxplemwb  36742  fperiodmul  37597  fsumnncl  37735  dvsinexp  37866  dvxpaek  37901  itgsinexplem1  37916  stoweidlem1  37962  stoweidlem17  37978  stoweidlem25  37986  stoweidlem34  37996  stoweidlem38  38000  stoweidlem40  38002  stoweidlem42  38004  stoweidlem45  38007  stirlinglem4  38040  stirlinglem5  38041  stirlinglem10  38046  stirlinglem13  38049  dirkertrigeq  38064  fourierdlem21  38091  fourierdlem25  38095  fourierdlem48  38119  fourierdlem54  38125  fourierdlem64  38135  fourierdlem65  38136  fourierdlem73  38144  fourierdlem81  38152  fourierdlem83  38154  fourierdlem92  38163  fourierdlem103  38174  fourierdlem104  38175  fourierdlem112  38183  fourierdlem113  38184  etransclem1  38201  etransclem4  38204  etransclem8  38208  etransclem15  38215  etransclem17  38217  etransclem18  38218  etransclem19  38219  etransclem20  38220  etransclem21  38221  etransclem22  38222  etransclem23  38223  etransclem24  38224  etransclem25  38225  etransclem27  38227  etransclem32  38232  etransclem35  38235  etransclem41  38241  etransclem44  38244  etransclem46  38246  iccpartigtl  38872  iccpartgt  38876  iccpartgel  38878  iccelpart  38882  perfectALTVlem1  38978  perfectALTVlem2  38979  perfectALTV  38980  proththdlem  39048  proththd  39049  logbpw2m1  40747  nnpw2blenfzo  40761  nnolog2flm1  40770  dignn0fr  40781  nn0sumshdiglemA  40799  nn0sumshdiglemB  40800