Theorem nnnn0d 10628

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

Syntax hints:   -> wi 4   e. wcel 1756   NNcn 10314   NN0cn0 10571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-un 3328  df-in 3330  df-ss 3337  df-n0 10572

This theorem is referenced by:  nnzd  10738  expgt1  11894  expaddzlem  11899  expaddz  11900  expmulz  11902  expmulnbnd  11988  facwordi  12057  faclbnd  12058  facavg  12069  bcm1k  12083  wrdeqs1cat  12361  isercolllem2  13135  bcxmas  13290  climcndslem1  13304  climcndslem2  13305  climcnds  13306  geo2sum  13325  mertenslem1  13336  eftabs  13353  efcllem  13355  eftlub  13385  eirrlem  13478  rpnnen2lem9  13497  rpnnen2lem11  13499  dvdsfac  13580  bitsfzo  13623  bitsfi  13625  sadcaddlem  13645  smumullem  13680  gcdcl  13693  mulgcd  13722  rplpwr  13732  rppwr  13733  nprmdvds1  13789  isprm5  13790  rpexp  13798  zsqrelqelz  13828  dfphi2  13841  phiprmpw  13843  eulerthlem2  13849  eulerth  13850  fermltl  13851  odzcllem  13856  odzdvds  13859  odzphi  13860  pythagtriplem6  13880  pythagtriplem7  13881  pcprmpw2  13940  pcprod  13949  pcfac  13953  pcbc  13954  expnprm  13956  pockthlem  13958  pockthg  13959  prmunb  13967  prmreclem2  13970  prmreclem3  13971  prmreclem4  13972  prmreclem5  13973  prmreclem6  13974  mul4sqlem  14006  4sqlem11  14008  4sqlem17  14014  vdwlem1  14034  vdwlem5  14038  vdwlem6  14039  vdwlem8  14041  vdwlem9  14042  vdwlem11  14044  vdwlem12  14045  vdwnnlem3  14050  ramz2  14077  ramub1lem1  14079  ramub1lem2  14080  ramub1  14081  2expltfac  14111  psgnunilem3  15993  mndodconglem  16035  gexcl3  16077  pgpfi1  16085  sylow1lem1  16088  gexexlem  16325  prmcyg  16361  gsumval3OLD  16373  gsumval3  16376  ablfacrplem  16556  ablfacrp  16557  ablfacrp2  16558  ablfac1eu  16564  srgbinomlem3  16630  srgbinomlem4  16631  ovoliunlem1  20965  mbfi1fseqlem1  21173  mbfi1fseqlem3  21175  mbfi1fseqlem5  21177  itg2cnlem2  21220  dvply1  21730  aalioulem2  21779  aalioulem5  21782  aaliou3lem1  21788  aaliou3lem2  21789  aaliou3lem8  21791  aaliou3lem6  21794  taylthlem1  21818  taylthlem2  21819  pserdvlem2  21873  cxpeq  22175  wilthlem1  22386  ftalem1  22390  ftalem2  22391  ftalem4  22393  ftalem5  22394  basellem2  22399  basellem3  22400  basellem4  22401  basellem5  22402  isppw2  22433  dvdsmulf1o  22514  sgmmul  22520  chpchtsum  22538  logfacubnd  22540  mersenne  22546  perfect1  22547  perfectlem1  22548  perfectlem2  22549  perfect  22550  dchrelbas3  22557  dchrelbasd  22558  dchrzrh1  22563  dchrzrhmul  22565  dchrmulcl  22568  dchrn0  22569  dchrfi  22574  dchrghm  22575  dchrabs  22579  dchrinv  22580  dchrptlem1  22583  dchrptlem2  22584  dchrptlem3  22585  dchrpt  22586  dchrsum2  22587  sum2dchr  22593  pcbcctr  22595  bcmono  22596  bclbnd  22599  bposlem1  22603  bposlem3  22605  bposlem5  22607  bposlem6  22608  lgslem1  22615  lgslem4  22618  lgsval2lem  22625  lgsvalmod  22634  lgsmod  22640  lgsdirprm  22648  lgsne0  22652  lgsqrlem1  22660  lgsqrlem2  22661  lgsqrlem3  22662  lgsqrlem4  22663  lgseisenlem1  22668  lgseisenlem2  22669  lgseisenlem3  22670  lgseisenlem4  22671  lgseisen  22672  lgsquadlem2  22674  lgsquadlem3  22675  m1lgs  22681  2sqlem3  22685  2sqblem  22696  chebbnd1lem1  22698  chebbnd1lem3  22700  rplogsumlem2  22714  rpvmasumlem  22716  dchrisumlem1  22718  dchrisumlem2  22719  dchrmusum2  22723  dchrvmasumlem3  22728  dchrisum0ff  22736  dchrisum0flblem1  22737  rpvmasum2  22741  dchrisum0re  22742  dchrisum0lem2a  22746  dirith  22758  mudivsum  22759  pntpbnd1a  22814  pntlemq  22830  pntlemr  22831  pntlemj  22832  ostth2lem2  22863  ostth2lem3  22864  ostth2  22866  dipcl  24078  dipcn  24086  sspival  24104  bcm1n  26047  isarchi2  26170  submarchi  26171  nexple  26417  oddpwdc  26706  eulerpartlemsv2  26710  eulerpartlemsf  26711  eulerpartlems  26712  eulerpartlemv  26716  eulerpartlemb  26720  plymulx0  26917  signsvtn0  26940  dmgmdivn0  26983  lgamgulmlem5  26988  lgamcvg2  27010  subfacp1lem1  27036  subfacp1lem6  27042  subfaclim  27045  erdszelem8  27055  erdszelem10  27057  cvmliftlem10  27152  prodmolem3  27415  prodmolem2a  27416  faclim2  27523  bpolydiflem  28166  nninfnub  28618  bfplem1  28692  3rexfrabdioph  29106  4rexfrabdioph  29107  6rexfrabdioph  29108  7rexfrabdioph  29109  irrapxlem5  29138  pellexlem2  29142  pellexlem6  29146  pell14qrgt0  29171  pell1qrge1  29182  pellfundgt1  29195  ltrmxnn0  29263  jm2.26lem3  29321  jm2.27a  29325  jm2.27c  29327  rmxdiophlem  29335  jm3.1lem1  29337  jm3.1lem2  29338  jm3.1lem3  29339  jm3.1  29340  dgrsub2  29462  mpaaeu  29478  idomsubgmo  29534  dvsinexp  29758  itgsinexplem1  29765  stoweidlem1  29767  stoweidlem17  29783  stoweidlem25  29791  stoweidlem34  29800  stoweidlem38  29804  stoweidlem40  29806  stoweidlem42  29808  stoweidlem45  29811  stirlinglem4  29843  stirlinglem5  29844  stirlinglem10  29849  stirlinglem13  29852  nn0ge2m1nn0  30156  eluzge2nn0  30163  erclwwlktr0  30450  hashecclwwlkn1  30479  usghashecclwwlk  30480  hashclwwlkn  30481  clwwlkndivn  30482  clwlkfclwwlk  30488  numclwwlk3  30673  numclwwlk6  30677  numclwwlk7  30678