Theorem nnnn0d 12613

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℕcn 12293  ℕ₀cn0 12553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-n0 12554

This theorem is referenced by:  nn0ge2m1nn0  12623  nnzd  12666  eluzge2nn0  12952  expgt1  14151  expaddzlem  14156  expaddz  14157  expmulz  14159  expmulnbnd  14284  exp11nnd  14310  facwordi  14338  faclbnd  14339  facavg  14350  bcm1k  14364  wrdeqs1cat  14768  cshwcsh2id  14877  relexpsucnnr  15074  isercolllem2  15714  bcxmas  15883  climcndslem1  15897  climcndslem2  15898  climcnds  15899  pwdif  15916  geo2sum  15921  mertenslem1  15932  prodmolem3  15981  prodmolem2a  15982  bpolydiflem  16102  eftabs  16123  efcllem  16125  eftlub  16157  eirrlem  16252  rpnnen2lem9  16270  rpnnen2lem11  16272  dvdsfac  16374  pwp1fsum  16439  oddpwp1fsum  16440  bitsfzo  16481  bitsfi  16483  sadcaddlem  16503  smumullem  16538  gcdcl  16552  dvdsgcdidd  16584  mulgcd  16595  rplpwr  16605  rprpwr  16606  rppwr  16607  nn0rppwr  16608  expgcd  16610  lcmcl  16648  lcmgcdnn  16658  lcmfcl  16675  nprmdvds1  16753  rpexp  16769  prmdvdsbc  16773  zsqrtelqelz  16805  phiprmpw  16823  eulerthlem2  16829  eulerth  16830  fermltl  16831  odzcllem  16839  odzdvds  16842  odzphi  16843  prm23lt5  16861  pythagtriplem6  16868  pythagtriplem7  16869  pcprmpw2  16929  dvdsprmpweqle  16933  pcprod  16942  pcfac  16946  pcbc  16947  expnprm  16949  pockthlem  16952  pockthg  16953  prmunb  16961  prmreclem2  16964  prmreclem3  16965  prmreclem4  16966  prmreclem5  16967  prmreclem6  16968  mul4sqlem  17000  4sqlem11  17002  4sqlem17  17008  vdwlem1  17028  vdwlem5  17032  vdwlem6  17033  vdwlem8  17035  vdwlem9  17036  vdwlem11  17038  vdwlem12  17039  vdwnnlem3  17044  ramz2  17071  ramub1lem1  17073  ramub1lem2  17074  ramub1  17075  prmgaplem3  17100  2expltfac  17140  psgnunilem3  19538  odfval  19574  mndodconglem  19583  gexcl3  19629  pgpfi1  19637  sylow1lem1  19640  gexexlem  19894  prmcyg  19936  gsumval3  19949  ablfacrplem  20109  ablfacrp  20110  ablfacrp2  20111  ablfac1eu  20117  prmgrpsimpgd  20158  srgbinomlem3  20255  srgbinomlem4  20256  fermltlchr  21567  freshmansdream  21616  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  cpmadugsumlemF  22903  ovoliunlem1  25556  mbfi1fseqlem1  25770  mbfi1fseqlem3  25772  mbfi1fseqlem5  25774  itg2cnlem2  25817  dvply1  26343  aalioulem2  26393  aalioulem5  26396  aaliou3lem1  26402  aaliou3lem2  26403  aaliou3lem8  26405  aaliou3lem6  26408  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  pserdvlem2  26490  cxpeq  26818  zrtelqelz  26819  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  27263  fsumvma2  27276  chpchtsum  27281  logfacubnd  27283  mersenne  27289  perfect1  27290  perfectlem1  27291  perfectlem2  27292  perfect  27293  dchrelbas3  27300  dchrelbasd  27301  dchrzrh1  27306  dchrzrhmul  27308  dchrmulcl  27311  dchrn0  27312  dchrfi  27317  dchrghm  27318  dchrabs  27322  dchrinv  27323  dchrptlem1  27326  dchrptlem2  27327  dchrptlem3  27328  dchrpt  27329  dchrsum2  27330  sum2dchr  27336  pcbcctr  27338  bcmono  27339  bclbnd  27342  bposlem1  27346  bposlem3  27348  bposlem5  27350  bposlem6  27351  lgslem1  27359  lgsval2lem  27369  lgsvalmod  27378  lgsmod  27385  lgsdirprm  27393  lgsne0  27397  lgsqrlem1  27408  lgsqrlem2  27409  lgsqrlem3  27410  lgsqrlem4  27411  gausslemma2dlem0b  27419  gausslemma2dlem0c  27420  gausslemma2dlem1  27428  gausslemma2dlem7  27435  gausslemma2d  27436  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem3  27439  lgseisenlem4  27440  lgseisen  27441  lgsquadlem2  27443  lgsquadlem3  27444  m1lgs  27450  2lgslem1a  27453  2sqlem3  27482  2sqblem  27493  chebbnd1lem1  27531  chebbnd1lem3  27533  rplogsumlem2  27547  rpvmasumlem  27549  dchrisumlem1  27551  dchrisumlem2  27552  dchrmusum2  27556  dchrvmasumlem3  27561  dchrisum0ff  27569  dchrisum0flblem1  27570  rpvmasum2  27574  dchrisum0re  27575  dchrisum0lem2a  27579  dirith  27591  mudivsum  27592  pntpbnd1a  27647  pntlemq  27663  pntlemr  27664  pntlemj  27665  ostth2lem1  27680  ostth2lem2  27696  ostth2lem3  27697  ostth2  27699  crctcshwlkn0lem6  29848  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  clwwlknon  30122  eucrctshift  30275  numclwlk1lem2  30402  nrt2irr  30505  dipcl  30744  dipcn  30752  bcm1n  32800  expgt0b  32820  wrdpmtrlast  33086  psgnfzto1st  33098  isarchi2  33165  submarchi  33166  znfermltl  33359  submateqlem1  33753  madjusmdetlem2  33774  madjusmdetlem4  33776  mdetlap  33778  nexple  33973  oddpwdc  34319  eulerpartlemsv2  34323  eulerpartlemsf  34324  eulerpartlems  34325  eulerpartlemv  34329  eulerpartlemb  34333  plymulx0  34524  signsvtn0  34547  fsum2dsub  34584  reprinfz1  34599  reprpmtf1o  34603  circlemeth  34617  circlemethnat  34618  hgt750lemb  34633  hgt750lema  34634  hgt750leme  34635  tgoldbachgtde  34637  tgoldbachgtda  34638  lpadleft  34660  subfacp1lem1  35147  subfacp1lem6  35153  subfaclim  35156  erdszelem8  35166  erdszelem10  35168  cvmliftlem10  35262  faclim2  35710  poimirlem7  37587  poimirlem17  37597  poimirlem18  37598  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  poimirlem32  37612  nninfnub  37711  bfplem1  37782  zndvdchrrhm  41927  lcmineqlem1  41986  lcmineqlem2  41987  lcmineqlem8  41993  lcmineqlem10  41995  lcmineqlem11  41996  lcmineqlem15  42000  lcmineqlem16  42001  lcmineqlem18  42003  lcmineqlem19  42004  lcmineqlem20  42005  lcmineqlem21  42006  lcmineqlem22  42007  3lexlogpow2ineq2  42016  dvrelogpow2b  42025  aks4d1p1p2  42027  aks4d1p1p4  42028  aks4d1p1  42033  aks4d1p3  42035  aks4d1p7d1  42039  aks4d1p7  42040  aks4d1p8  42044  aks4d1p9  42045  isprimroot2  42051  primrootsunit1  42054  primrootscoprmpow  42056  posbezout  42057  primrootscoprbij  42059  primrootlekpowne0  42062  primrootspoweq0  42063  aks6d1c1p2  42066  aks6d1c1p3  42067  aks6d1c1p4  42068  aks6d1c1p5  42069  aks6d1c1p7  42070  aks6d1c1p6  42071  aks6d1c1p8  42072  aks6d1c2p2  42076  hashscontpowcl  42077  hashscontpow1  42078  hashscontpow  42079  aks6d1c4  42081  aks6d1c2lem3  42083  aks6d1c2lem4  42084  aks6d1c2  42087  sticksstones6  42108  sticksstones7  42109  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  sticksstones20  42123  sticksstones22  42125  aks6d1c6lem2  42128  aks6d1c6lem3  42129  aks6d1c6lem4  42130  aks6d1c6isolem1  42131  aks6d1c6isolem2  42132  aks6d1c6lem5  42134  bcled  42135  bcle2d  42136  aks6d1c7lem1  42137  aks6d1c7  42141  aks5lem2  42144  aks5lem3a  42146  aks5lem5a  42148  grpods  42151  unitscyglem2  42153  unitscyglem4  42155  aks5lem7  42157  aks5  42161  metakunt2  42163  sumcubes  42301  oexpreposd  42309  exp11d  42313  dvdsexpb  42322  fiabv  42491  fsuppind  42545  dffltz  42589  fltdvdsabdvdsc  42593  fltne  42599  flt4lem4  42604  flt4lem7  42614  fltltc  42616  fltnltalem  42617  fltnlta  42618  3rexfrabdioph  42753  4rexfrabdioph  42754  6rexfrabdioph  42755  7rexfrabdioph  42756  irrapxlem5  42782  pellexlem2  42786  pellexlem6  42790  pell14qrgt0  42815  pell1qrge1  42826  pellfundgt1  42839  ltrmxnn0  42906  jm2.26lem3  42958  jm2.27a  42962  jm2.27c  42964  rmxdiophlem  42972  jm3.1lem1  42974  jm3.1lem2  42975  jm3.1lem3  42976  jm3.1  42977  dgrsub2  43092  mpaaeu  43107  idomsubgmo  43154  relexpxpmin  43679  nzprmdif  44288  binomcxplemwb  44317  fperiodmul  45219  xralrple4  45288  fsumnncl  45493  dvsinexp  45832  dvxpaek  45861  itgsinexplem1  45875  stoweidlem1  45922  stoweidlem17  45938  stoweidlem25  45946  stoweidlem34  45955  stoweidlem38  45959  stoweidlem40  45961  stoweidlem42  45963  stoweidlem45  45966  stirlinglem4  45998  stirlinglem5  45999  stirlinglem10  46004  stirlinglem13  46007  dirkertrigeq  46022  fourierdlem21  46049  fourierdlem25  46053  fourierdlem48  46075  fourierdlem54  46081  fourierdlem64  46091  fourierdlem65  46092  fourierdlem73  46100  fourierdlem81  46108  fourierdlem83  46110  fourierdlem92  46119  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  fourierdlem113  46140  etransclem1  46156  etransclem4  46159  etransclem8  46163  etransclem15  46170  etransclem17  46172  etransclem18  46173  etransclem19  46174  etransclem20  46175  etransclem21  46176  etransclem22  46177  etransclem23  46178  etransclem24  46179  etransclem25  46180  etransclem27  46182  etransclem32  46187  etransclem35  46190  etransclem41  46196  etransclem44  46199  etransclem46  46201  iccpartigtl  47297  iccpartgt  47301  iccpartgel  47303  iccelpart  47307  odz2prm2pw  47437  fmtnoprmfac1  47439  fmtnoprmfac2  47441  2pwp1prm  47463  sfprmdvdsmersenne  47477  lighneallem4a  47482  proththdlem  47487  proththd  47488  perfectALTVlem1  47595  perfectALTVlem2  47596  perfectALTV  47597  fpprwpprb  47614  logbpw2m1  48301  nnpw2blenfzo  48315  nnolog2flm1  48324  dignn0fr  48335  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354