Theorem nnnn0d 12542

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 12484	. 2 ⊢ ℕ ⊆ ℕ0
2		nnnn0d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3934	1 ⊢ (𝜑 → 𝐴 ∈ ℕ0)

Syntax hints:   → wi 4   ∈ wcel 2142  ℕcn 12210  ℕ₀cn0 12481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921  df-n0 12482

This theorem is referenced by:  nn0ge2m1nn0  12552  nnzd  12594  eluzge2nn0  12893  expgt1  14113  expaddzlem  14118  expaddz  14119  expmulz  14121  expmulnbnd  14248  exp11nnd  14274  facwordi  14302  faclbnd  14303  facavg  14314  bcm1k  14328  wrdeqs1cat  14733  cshwcsh2id  14841  relexpsucnnr  15038  isercolllem2  15693  bcxmas  15865  climcndslem1  15879  climcndslem2  15880  climcnds  15881  pwdif  15898  geo2sum  15903  mertenslem1  15914  prodmolem3  15963  prodmolem2a  15964  bpolydiflem  16084  eftabs  16105  efcllem  16107  eftlub  16141  eirrlem  16236  rpnnen2lem9  16254  rpnnen2lem11  16256  dvdsfac  16360  pwp1fsum  16425  oddpwp1fsum  16426  bitsfzo  16469  bitsfi  16471  sadcaddlem  16491  smumullem  16526  gcdcl  16540  dvdsgcdidd  16571  mulgcd  16582  rplpwr  16592  rprpwr  16593  rppwr  16594  nn0rppwr  16595  expgcd  16597  lcmcl  16635  lcmgcdnn  16645  lcmfcl  16662  nprmdvds1  16741  rpexp  16757  prmdvdsbc  16761  zsqrtelqelz  16793  phiprmpw  16811  eulerthlem2  16817  eulerth  16818  fermltl  16819  odzcllem  16828  odzdvds  16831  odzphi  16832  prm23lt5  16850  pythagtriplem6  16857  pythagtriplem7  16858  pcprmpw2  16918  dvdsprmpweqle  16922  pcprod  16931  pcfac  16935  pcbc  16936  expnprm  16938  pockthlem  16941  pockthg  16942  prmunb  16950  prmreclem2  16953  prmreclem3  16954  prmreclem4  16955  prmreclem5  16956  prmreclem6  16957  mul4sqlem  16989  4sqlem11  16991  4sqlem17  16997  vdwlem1  17017  vdwlem5  17021  vdwlem6  17022  vdwlem8  17024  vdwlem9  17025  vdwlem11  17027  vdwlem12  17028  vdwnnlem3  17033  ramz2  17060  ramub1lem1  17062  ramub1lem2  17063  ramub1  17064  prmgaplem3  17089  2expltfac  17128  psgnunilem3  19536  odfval  19572  mndodconglem  19581  gexcl3  19627  pgpfi1  19635  sylow1lem1  19638  gexexlem  19892  prmcyg  19934  gsumval3  19947  ablfacrplem  20107  ablfacrp  20108  ablfacrp2  20109  ablfac1eu  20115  prmgrpsimpgd  20156  srgbinomlem3  20274  srgbinomlem4  20275  fermltlchr  21578  freshmansdream  21623  chfacfscmulgsum  22917  chfacfpmmulgsum  22921  cpmadugsumlemF  22933  ovoliunlem1  25561  mbfi1fseqlem1  25774  mbfi1fseqlem3  25776  mbfi1fseqlem5  25778  itg2cnlem2  25821  plyn0mulidp  26342  dvply1  26345  aalioulem2  26394  aalioulem5  26397  aaliou3lem1  26403  aaliou3lem2  26404  aaliou3lem8  26406  aaliou3lem6  26409  taylthlem1  26433  taylthlem2  26434  pserdvlem2  26488  cxpeq  26819  zrtelqelz  26820  dmgmdivn0  27089  lgamgulmlem5  27094  lgamcvg2  27116  wilthlem1  27129  ftalem1  27134  ftalem2  27135  ftalem4  27137  ftalem5  27138  basellem2  27143  basellem3  27144  basellem4  27145  basellem5  27146  isppw2  27176  mpodvdsmulf1o  27255  dvdsmulf1o  27257  sgmmul  27262  fsumvma2  27275  chpchtsum  27280  logfacubnd  27282  mersenne  27288  perfect1  27289  perfectlem1  27290  perfectlem2  27291  perfect  27292  dchrelbas3  27299  dchrelbasd  27300  dchrzrh1  27305  dchrzrhmul  27307  dchrmulcl  27310  dchrn0  27311  dchrfi  27316  dchrghm  27317  dchrabs  27321  dchrinv  27322  dchrptlem1  27325  dchrptlem2  27326  dchrptlem3  27327  dchrpt  27328  dchrsum2  27329  sum2dchr  27335  pcbcctr  27337  bcmono  27338  bclbnd  27341  bposlem1  27345  bposlem3  27347  bposlem5  27349  bposlem6  27350  lgslem1  27358  lgsval2lem  27368  lgsvalmod  27377  lgsmod  27384  lgsdirprm  27392  lgsne0  27396  lgsqrlem1  27407  lgsqrlem2  27408  lgsqrlem3  27409  lgsqrlem4  27410  gausslemma2dlem0b  27418  gausslemma2dlem0c  27419  gausslemma2dlem1  27427  gausslemma2dlem7  27434  gausslemma2d  27435  lgseisenlem1  27436  lgseisenlem2  27437  lgseisenlem3  27438  lgseisenlem4  27439  lgseisen  27440  lgsquadlem2  27442  lgsquadlem3  27443  m1lgs  27449  2lgslem1a  27452  2sqlem3  27481  2sqblem  27492  chebbnd1lem1  27530  chebbnd1lem3  27532  rplogsumlem2  27546  rpvmasumlem  27548  dchrisumlem1  27550  dchrisumlem2  27551  dchrmusum2  27555  dchrvmasumlem3  27560  dchrisum0ff  27568  dchrisum0flblem1  27569  rpvmasum2  27573  dchrisum0re  27574  dchrisum0lem2a  27578  dirith  27590  mudivsum  27591  pntpbnd1a  27646  pntlemq  27662  pntlemr  27663  pntlemj  27664  ostth2lem1  27679  ostth2lem2  27695  ostth2lem3  27696  ostth2  27698  crctcshwlkn0lem6  30012  hashecclwwlkn1  30276  umgrhashecclwwlk  30277  clwwlknon  30289  eucrctshift  30442  numclwlk1lem2  30569  nrt2irr  30672  dipcl  30912  dipcn  30920  bcm1n  32994  expgt0b  33016  nexple  33032  2exple2exp  33033  oexpled  33035  wrdpmtrlast  33270  psgnfzto1st  33282  isarchi2  33362  submarchi  33363  znfermltl  33549  fldextrspundgdvdslem  33974  fldextrspundgdvds  33975  fldext2rspun  33976  constrext2chnlem  34044  cos9thpiminplylem2  34077  submateqlem1  34101  madjusmdetlem2  34122  madjusmdetlem4  34124  mdetlap  34126  oddpwdc  34648  eulerpartlemsv2  34652  eulerpartlemsf  34653  eulerpartlems  34654  eulerpartlemv  34658  eulerpartlemb  34662  signsvtn0  34861  fsum2dsub  34898  reprinfz1  34913  reprpmtf1o  34917  circlemeth  34931  circlemethnat  34932  hgt750lemb  34947  hgt750lema  34948  hgt750leme  34949  tgoldbachgtde  34951  tgoldbachgtda  34952  lpadleft  34977  subfacp1lem1  35526  subfacp1lem6  35532  subfaclim  35535  erdszelem8  35545  erdszelem10  35547  cvmliftlem10  35641  faclim2  36095  poimirlem7  38123  poimirlem17  38133  poimirlem18  38134  poimirlem20  38136  poimirlem21  38137  poimirlem22  38138  poimirlem25  38141  poimirlem26  38142  poimirlem27  38143  poimirlem28  38144  poimirlem32  38148  nninfnub  38247  bfplem1  38318  zndvdchrrhm  42587  lcmineqlem1  42643  lcmineqlem2  42644  lcmineqlem8  42650  lcmineqlem10  42652  lcmineqlem11  42653  lcmineqlem15  42657  lcmineqlem16  42658  lcmineqlem18  42660  lcmineqlem19  42661  lcmineqlem20  42662  lcmineqlem21  42663  lcmineqlem22  42664  3lexlogpow2ineq2  42673  dvrelogpow2b  42682  aks4d1p1p2  42684  aks4d1p1p4  42685  aks4d1p1  42690  aks4d1p3  42692  aks4d1p7d1  42696  aks4d1p7  42697  aks4d1p8  42701  aks4d1p9  42702  isprimroot2  42708  primrootsunit1  42711  primrootscoprmpow  42713  posbezout  42714  primrootscoprbij  42716  primrootlekpowne0  42719  primrootspoweq0  42720  aks6d1c1p2  42723  aks6d1c1p3  42724  aks6d1c1p4  42725  aks6d1c1p5  42726  aks6d1c1p7  42727  aks6d1c1p6  42728  aks6d1c1p8  42729  aks6d1c2p2  42733  hashscontpowcl  42734  hashscontpow1  42735  hashscontpow  42736  aks6d1c4  42738  aks6d1c2lem3  42740  aks6d1c2lem4  42741  aks6d1c2  42744  sticksstones6  42765  sticksstones7  42766  sticksstones10  42769  sticksstones12a  42771  sticksstones12  42772  sticksstones20  42780  sticksstones22  42782  aks6d1c6lem2  42785  aks6d1c6lem3  42786  aks6d1c6lem4  42787  aks6d1c6isolem1  42788  aks6d1c6isolem2  42789  aks6d1c6lem5  42791  bcled  42792  bcle2d  42793  aks6d1c7lem1  42794  aks6d1c7  42798  aks5lem2  42801  aks5lem3a  42803  aks5lem5a  42805  grpods  42808  unitscyglem2  42810  unitscyglem4  42812  aks5lem7  42814  aks5  42818  sumcubes  42919  oexpreposd  42928  exp11d  42932  dvdsexpb  42941  fiabv  43151  fsuppind  43169  dffltz  43213  fltdvdsabdvdsc  43217  fltne  43223  flt4lem4  43228  flt4lem7  43238  fltltc  43240  fltnltalem  43241  fltnlta  43242  3rexfrabdioph  43371  4rexfrabdioph  43372  6rexfrabdioph  43373  7rexfrabdioph  43374  irrapxlem5  43400  pellexlem2  43404  pellexlem6  43408  pell14qrgt0  43433  pell1qrge1  43444  pellfundgt1  43457  ltrmxnn0  43523  jm2.26lem3  43575  jm2.27a  43579  jm2.27c  43581  rmxdiophlem  43589  jm3.1lem1  43591  jm3.1lem2  43592  jm3.1lem3  43593  jm3.1  43594  dgrsub2  43709  mpaaeu  43724  idomsubgmo  43767  relexpxpmin  44290  nzprmdif  44892  binomcxplemwb  44921  fperiodmul  45880  xralrple4  45945  fsumnncl  46145  dvsinexp  46482  dvxpaek  46511  itgsinexplem1  46525  stoweidlem1  46572  stoweidlem17  46588  stoweidlem25  46596  stoweidlem34  46605  stoweidlem38  46609  stoweidlem40  46611  stoweidlem42  46613  stoweidlem45  46616  stirlinglem4  46648  stirlinglem5  46649  stirlinglem10  46654  stirlinglem13  46657  dirkertrigeq  46672  fourierdlem21  46699  fourierdlem25  46703  fourierdlem48  46725  fourierdlem54  46731  fourierdlem64  46741  fourierdlem65  46742  fourierdlem73  46750  fourierdlem81  46758  fourierdlem83  46760  fourierdlem92  46769  fourierdlem103  46780  fourierdlem104  46781  fourierdlem112  46789  fourierdlem113  46790  etransclem1  46806  etransclem4  46809  etransclem8  46813  etransclem15  46820  etransclem17  46822  etransclem18  46823  etransclem19  46824  etransclem20  46825  etransclem21  46826  etransclem22  46827  etransclem23  46828  etransclem24  46829  etransclem25  46830  etransclem27  46832  etransclem32  46837  etransclem35  46840  etransclem41  46846  etransclem44  46849  etransclem46  46851  modmknepk  47959  iccpartigtl  48026  iccpartgt  48030  iccpartgel  48032  iccelpart  48036  odz2prm2pw  48169  fmtnoprmfac1  48171  fmtnoprmfac2  48173  2pwp1prm  48195  sfprmdvdsmersenne  48209  lighneallem4a  48214  proththdlem  48219  proththd  48220  perfectALTVlem1  48340  perfectALTVlem2  48341  perfectALTV  48342  fpprwpprb  48359  gpgedgvtx1  48681  logbpw2m1  49186  nnpw2blenfzo  49200  nnolog2flm1  49209  dignn0fr  49220  nn0sumshdiglemA  49238  nn0sumshdiglemB  49239