Theorem nnnn0d 10230

Description: A natural number 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 10180	. 2 |- NN C_ NN0
2		nnnn0d.1	. 2 |- ( ph -> A e. NN )
3	1, 2	sseldi 3306	1 |- ( ph -> A e. NN0 )

Syntax hints:   -> wi 4   e. wcel 1721   NNcn 9956   NN0cn0 10177

This theorem is referenced by:  nnzd  10330  expgt1  11373  expaddzlem  11378  expaddz  11379  expmulz  11381  expmulnbnd  11466  facwordi  11535  faclbnd  11536  facavg  11547  bcm1k  11561  wrdeqs1cat  11744  isercolllem2  12414  bcxmas  12570  climcndslem1  12584  climcndslem2  12585  climcnds  12586  geo2sum  12605  mertenslem1  12616  eftabs  12633  efcllem  12635  eftlub  12665  eirrlem  12758  rpnnen2lem9  12777  rpnnen2lem11  12779  dvdsfac  12859  bitsfzo  12902  bitsfi  12904  sadcaddlem  12924  smumullem  12959  gcdcl  12972  mulgcd  13001  rplpwr  13011  rppwr  13012  nprmdvds1  13066  isprm5  13067  rpexp  13075  zsqrelqelz  13105  dfphi2  13118  phiprmpw  13120  eulerthlem2  13126  eulerth  13127  fermltl  13128  odzcllem  13133  odzdvds  13136  odzphi  13137  pythagtriplem6  13150  pythagtriplem7  13151  pcprmpw2  13210  pcprod  13219  pcfac  13223  pcbc  13224  expnprm  13226  pockthlem  13228  pockthg  13229  prmunb  13237  prmreclem2  13240  prmreclem3  13241  prmreclem4  13242  prmreclem5  13243  prmreclem6  13244  mul4sqlem  13276  4sqlem11  13278  4sqlem17  13284  vdwlem1  13304  vdwlem5  13308  vdwlem6  13309  vdwlem8  13311  vdwlem9  13312  vdwlem11  13314  vdwlem12  13315  vdwnnlem3  13320  ramz2  13347  ramub1lem1  13349  ramub1lem2  13350  ramub1  13351  2expltfac  13381  mndodconglem  15134  gexcl3  15176  pgpfi1  15184  sylow1lem1  15187  gexexlem  15422  prmcyg  15458  gsumval3  15469  ablfacrplem  15578  ablfacrp  15579  ablfacrp2  15580  ablfac1eu  15586  ovoliunlem1  19351  mbfi1fseqlem1  19560  mbfi1fseqlem3  19562  mbfi1fseqlem5  19564  itg2cnlem2  19607  dvply1  20154  aalioulem2  20203  aalioulem5  20206  aaliou3lem1  20212  aaliou3lem2  20213  aaliou3lem8  20215  aaliou3lem6  20218  taylthlem1  20242  taylthlem2  20243  pserdvlem2  20297  cxpeq  20594  wilthlem1  20804  ftalem1  20808  ftalem2  20809  ftalem4  20811  ftalem5  20812  basellem2  20817  basellem3  20818  basellem4  20819  basellem5  20820  isppw2  20851  dvdsmulf1o  20932  sgmmul  20938  chpchtsum  20956  logfacubnd  20958  mersenne  20964  perfect1  20965  perfectlem1  20966  perfectlem2  20967  perfect  20968  dchrelbas3  20975  dchrelbasd  20976  dchrzrh1  20981  dchrzrhmul  20983  dchrmulcl  20986  dchrn0  20987  dchrfi  20992  dchrghm  20993  dchrabs  20997  dchrinv  20998  dchrptlem1  21001  dchrptlem2  21002  dchrptlem3  21003  dchrpt  21004  dchrsum2  21005  sum2dchr  21011  pcbcctr  21013  bcmono  21014  bclbnd  21017  bposlem1  21021  bposlem3  21023  bposlem5  21025  bposlem6  21026  lgslem1  21033  lgslem4  21036  lgsval2lem  21043  lgsvalmod  21052  lgsmod  21058  lgsdirprm  21066  lgsne0  21070  lgsqrlem1  21078  lgsqrlem2  21079  lgsqrlem3  21080  lgsqrlem4  21081  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem3  21088  lgseisenlem4  21089  lgseisen  21090  lgsquadlem2  21092  lgsquadlem3  21093  m1lgs  21099  2sqlem3  21103  2sqblem  21114  chebbnd1lem1  21116  chebbnd1lem3  21118  rplogsumlem2  21132  rpvmasumlem  21134  dchrisumlem1  21136  dchrisumlem2  21137  dchrmusum2  21141  dchrvmasumlem3  21146  dchrisum0ff  21154  dchrisum0flblem1  21155  rpvmasum2  21159  dchrisum0re  21160  dchrisum0lem2a  21164  dirith  21176  mudivsum  21177  pntpbnd1a  21232  pntlemq  21248  pntlemr  21249  pntlemj  21250  ostth2lem2  21281  ostth2lem3  21282  ostth2  21284  dipcl  22164  dipcn  22172  sspival  22190  bcm1n  24104  dmgmdivn0  24765  lgamgulmlem5  24770  lgamcvg2  24792  subfacp1lem1  24818  subfacp1lem6  24824  subfaclim  24827  erdszelem8  24837  erdszelem10  24839  cvmliftlem10  24934  prodmolem3  25212  prodmolem2a  25213  faclim2  25315  bpolydiflem  26004  nninfnub  26345  bfplem1  26421  3rexfrabdioph  26747  4rexfrabdioph  26748  6rexfrabdioph  26749  7rexfrabdioph  26750  irrapxlem5  26779  pellexlem2  26783  pellexlem6  26787  pell14qrgt0  26812  pell1qrge1  26823  pellfundgt1  26836  ltrmxnn0  26904  jm2.26lem3  26962  jm2.27a  26966  jm2.27c  26968  rmxdiophlem  26976  jm3.1lem1  26978  jm3.1lem2  26979  jm3.1lem3  26980  jm3.1  26981  dgrsub2  27207  mpaaeu  27223  psgnunilem3  27287  idomsubgmo  27382  dvsinexp  27607  itgsinexplem1  27615  stoweidlem1  27617  stoweidlem17  27633  stoweidlem25  27641  stoweidlem34  27650  stoweidlem38  27654  stoweidlem40  27656  stoweidlem42  27658  stoweidlem45  27661  stirlinglem4  27693  stirlinglem5  27694  stirlinglem10  27699  stirlinglem13  27702

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285  df-in 3287  df-ss 3294  df-n0 10178