Theorem nnnn0d 12532

Description: A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnnn0d.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnnn0d	⊢ (𝜑 → 𝐴 ∈ ℕ0)

Proof of Theorem nnnn0d

Step	Hyp	Ref	Expression
1		nnssnn0 12475	. 2 ⊢ ℕ ⊆ ℕ0
2		nnnn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3981	1 ⊢ (𝜑 → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2107  ℕcn 12212  ℕ₀cn0 12472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-n0 12473

This theorem is referenced by:  nn0ge2m1nn0  12542  nnzd  12585  eluzge2nn0  12871  expgt1  14066  expaddzlem  14071  expaddz  14072  expmulz  14074  expmulnbnd  14198  facwordi  14249  faclbnd  14250  facavg  14261  bcm1k  14275  wrdeqs1cat  14670  cshwcsh2id  14779  relexpsucnnr  14972  isercolllem2  15612  bcxmas  15781  climcndslem1  15795  climcndslem2  15796  climcnds  15797  pwdif  15814  geo2sum  15819  mertenslem1  15830  prodmolem3  15877  prodmolem2a  15878  bpolydiflem  15998  eftabs  16019  efcllem  16021  eftlub  16052  eirrlem  16147  rpnnen2lem9  16165  rpnnen2lem11  16167  dvdsfac  16269  pwp1fsum  16334  oddpwp1fsum  16335  bitsfzo  16376  bitsfi  16378  sadcaddlem  16398  smumullem  16433  gcdcl  16447  dvdsgcdidd  16479  mulgcd  16490  rplpwr  16499  rprpwr  16500  rppwr  16501  lcmcl  16538  lcmgcdnn  16548  lcmfcl  16565  nprmdvds1  16643  rpexp  16659  zsqrtelqelz  16694  phiprmpw  16709  eulerthlem2  16715  eulerth  16716  fermltl  16717  odzcllem  16725  odzdvds  16728  odzphi  16729  prm23lt5  16747  pythagtriplem6  16754  pythagtriplem7  16755  pcprmpw2  16815  dvdsprmpweqle  16819  pcprod  16828  pcfac  16832  pcbc  16833  expnprm  16835  pockthlem  16838  pockthg  16839  prmunb  16847  prmreclem2  16850  prmreclem3  16851  prmreclem4  16852  prmreclem5  16853  prmreclem6  16854  mul4sqlem  16886  4sqlem11  16888  4sqlem17  16894  vdwlem1  16914  vdwlem5  16918  vdwlem6  16919  vdwlem8  16921  vdwlem9  16922  vdwlem11  16924  vdwlem12  16925  vdwnnlem3  16930  ramz2  16957  ramub1lem1  16959  ramub1lem2  16960  ramub1  16961  prmgaplem3  16986  2expltfac  17026  psgnunilem3  19364  odfval  19400  mndodconglem  19409  gexcl3  19455  pgpfi1  19463  sylow1lem1  19466  gexexlem  19720  prmcyg  19762  gsumval3  19775  ablfacrplem  19935  ablfacrp  19936  ablfacrp2  19937  ablfac1eu  19943  prmgrpsimpgd  19984  srgbinomlem3  20051  srgbinomlem4  20052  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  cpmadugsumlemF  22378  ovoliunlem1  25019  mbfi1fseqlem1  25233  mbfi1fseqlem3  25235  mbfi1fseqlem5  25237  itg2cnlem2  25280  dvply1  25797  aalioulem2  25846  aalioulem5  25849  aaliou3lem1  25855  aaliou3lem2  25856  aaliou3lem8  25858  aaliou3lem6  25861  taylthlem1  25885  taylthlem2  25886  pserdvlem2  25940  cxpeq  26265  dmgmdivn0  26532  lgamgulmlem5  26537  lgamcvg2  26559  wilthlem1  26572  ftalem1  26577  ftalem2  26578  ftalem4  26580  ftalem5  26581  basellem2  26586  basellem3  26587  basellem4  26588  basellem5  26589  isppw2  26619  dvdsmulf1o  26698  sgmmul  26704  fsumvma2  26717  chpchtsum  26722  logfacubnd  26724  mersenne  26730  perfect1  26731  perfectlem1  26732  perfectlem2  26733  perfect  26734  dchrelbas3  26741  dchrelbasd  26742  dchrzrh1  26747  dchrzrhmul  26749  dchrmulcl  26752  dchrn0  26753  dchrfi  26758  dchrghm  26759  dchrabs  26763  dchrinv  26764  dchrptlem1  26767  dchrptlem2  26768  dchrptlem3  26769  dchrpt  26770  dchrsum2  26771  sum2dchr  26777  pcbcctr  26779  bcmono  26780  bclbnd  26783  bposlem1  26787  bposlem3  26789  bposlem5  26791  bposlem6  26792  lgslem1  26800  lgsval2lem  26810  lgsvalmod  26819  lgsmod  26826  lgsdirprm  26834  lgsne0  26838  lgsqrlem1  26849  lgsqrlem2  26850  lgsqrlem3  26851  lgsqrlem4  26852  gausslemma2dlem0b  26860  gausslemma2dlem0c  26861  gausslemma2dlem1  26869  gausslemma2dlem7  26876  gausslemma2d  26877  lgseisenlem1  26878  lgseisenlem2  26879  lgseisenlem3  26880  lgseisenlem4  26881  lgseisen  26882  lgsquadlem2  26884  lgsquadlem3  26885  m1lgs  26891  2lgslem1a  26894  2sqlem3  26923  2sqblem  26934  chebbnd1lem1  26972  chebbnd1lem3  26974  rplogsumlem2  26988  rpvmasumlem  26990  dchrisumlem1  26992  dchrisumlem2  26993  dchrmusum2  26997  dchrvmasumlem3  27002  dchrisum0ff  27010  dchrisum0flblem1  27011  rpvmasum2  27015  dchrisum0re  27016  dchrisum0lem2a  27020  dirith  27032  mudivsum  27033  pntpbnd1a  27088  pntlemq  27104  pntlemr  27105  pntlemj  27106  ostth2lem1  27121  ostth2lem2  27137  ostth2lem3  27138  ostth2  27140  crctcshwlkn0lem6  29100  hashecclwwlkn1  29361  umgrhashecclwwlk  29362  clwwlknon  29374  eucrctshift  29527  numclwlk1lem2  29654  nrt2irr  29757  dipcl  29996  dipcn  30004  bcm1n  32037  prmdvdsbc  32053  psgnfzto1st  32295  isarchi2  32362  submarchi  32363  freshmansdream  32412  fermltlchr  32509  znfermltl  32510  submateqlem1  32818  madjusmdetlem2  32839  madjusmdetlem4  32841  mdetlap  32843  nexple  33038  oddpwdc  33384  eulerpartlemsv2  33388  eulerpartlemsf  33389  eulerpartlems  33390  eulerpartlemv  33394  eulerpartlemb  33398  plymulx0  33589  signsvtn0  33612  fsum2dsub  33650  reprinfz1  33665  reprpmtf1o  33669  circlemeth  33683  circlemethnat  33684  hgt750lemb  33699  hgt750lema  33700  hgt750leme  33701  tgoldbachgtde  33703  tgoldbachgtda  33704  lpadleft  33726  subfacp1lem1  34201  subfacp1lem6  34207  subfaclim  34210  erdszelem8  34220  erdszelem10  34222  cvmliftlem10  34316  faclim2  34749  poimirlem7  36543  poimirlem17  36553  poimirlem18  36554  poimirlem20  36556  poimirlem21  36557  poimirlem22  36558  poimirlem25  36561  poimirlem26  36562  poimirlem27  36563  poimirlem28  36564  poimirlem32  36568  nninfnub  36667  bfplem1  36738  lcmineqlem1  40942  lcmineqlem2  40943  lcmineqlem8  40949  lcmineqlem10  40951  lcmineqlem11  40952  lcmineqlem15  40956  lcmineqlem16  40957  lcmineqlem18  40959  lcmineqlem19  40960  lcmineqlem20  40961  lcmineqlem21  40962  lcmineqlem22  40963  3lexlogpow2ineq2  40972  dvrelogpow2b  40981  aks4d1p1p2  40983  aks4d1p1p4  40984  aks4d1p1  40989  aks4d1p3  40991  aks4d1p7d1  40995  aks4d1p7  40996  aks4d1p8  41000  aks4d1p9  41001  aks6d1c2p2  41005  sticksstones6  41015  sticksstones7  41016  sticksstones10  41019  sticksstones12a  41021  sticksstones12  41022  sticksstones20  41030  sticksstones22  41032  metakunt2  41034  fsuppind  41210  sumcubes  41259  oexpreposd  41260  exp11nnd  41263  exp11d  41264  nn0rppwr  41272  expgcd  41273  dvdsexpb  41281  zrtelqelz  41283  dffltz  41424  fltdvdsabdvdsc  41428  fltne  41434  flt4lem4  41439  flt4lem7  41449  fltltc  41451  fltnltalem  41452  fltnlta  41453  3rexfrabdioph  41583  4rexfrabdioph  41584  6rexfrabdioph  41585  7rexfrabdioph  41586  irrapxlem5  41612  pellexlem2  41616  pellexlem6  41620  pell14qrgt0  41645  pell1qrge1  41656  pellfundgt1  41669  ltrmxnn0  41736  jm2.26lem3  41788  jm2.27a  41792  jm2.27c  41794  rmxdiophlem  41802  jm3.1lem1  41804  jm3.1lem2  41805  jm3.1lem3  41806  jm3.1  41807  dgrsub2  41925  mpaaeu  41940  idomsubgmo  41988  relexpxpmin  42516  nzprmdif  43126  binomcxplemwb  43155  fperiodmul  44062  xralrple4  44131  fsumnncl  44336  dvsinexp  44675  dvxpaek  44704  itgsinexplem1  44718  stoweidlem1  44765  stoweidlem17  44781  stoweidlem25  44789  stoweidlem34  44798  stoweidlem38  44802  stoweidlem40  44804  stoweidlem42  44806  stoweidlem45  44809  stirlinglem4  44841  stirlinglem5  44842  stirlinglem10  44847  stirlinglem13  44850  dirkertrigeq  44865  fourierdlem21  44892  fourierdlem25  44896  fourierdlem48  44918  fourierdlem54  44924  fourierdlem64  44934  fourierdlem65  44935  fourierdlem73  44943  fourierdlem81  44951  fourierdlem83  44953  fourierdlem92  44962  fourierdlem103  44973  fourierdlem104  44974  fourierdlem112  44982  fourierdlem113  44983  etransclem1  44999  etransclem4  45002  etransclem8  45006  etransclem15  45013  etransclem17  45015  etransclem18  45016  etransclem19  45017  etransclem20  45018  etransclem21  45019  etransclem22  45020  etransclem23  45021  etransclem24  45022  etransclem25  45023  etransclem27  45025  etransclem32  45030  etransclem35  45033  etransclem41  45039  etransclem44  45042  etransclem46  45044  iccpartigtl  46139  iccpartgt  46143  iccpartgel  46145  iccelpart  46149  odz2prm2pw  46279  fmtnoprmfac1  46281  fmtnoprmfac2  46283  2pwp1prm  46305  sfprmdvdsmersenne  46319  lighneallem4a  46324  proththdlem  46329  proththd  46330  perfectALTVlem1  46437  perfectALTVlem2  46438  perfectALTV  46439  fpprwpprb  46456  logbpw2m1  47301  nnpw2blenfzo  47315  nnolog2flm1  47324  dignn0fr  47335  nn0sumshdiglemA  47353  nn0sumshdiglemB  47354