Theorem nnnn0d 12593

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℕcn 12261  ℕ₀cn0 12532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919  df-n0 12533

This theorem is used by:  nn0ge2m1nn0  12603  nnzd  12645  eluzge2nn0  12945  expgt1  14168  expaddzlem  14173  expaddz  14174  expmulz  14176  expmulnbnd  14303  exp11nnd  14329  facwordi  14357  faclbnd  14358  facavg  14369  bcm1k  14383  wrdeqs1cat  14793  cshwcsh2id  14903  relexpsucnnr  15102  isercolllem2  15757  bcxmas  15928  climcndslem1  15942  climcndslem2  15943  climcnds  15944  pwdif  15961  geo2sum  15966  mertenslem1  15977  prodmolem3  16026  prodmolem2a  16027  bpolydiflem  16146  eftabs  16167  efcllem  16169  eftlub  16203  eirrlem  16298  rpnnen2lem9  16316  rpnnen2lem11  16318  dvdsfac  16422  pwp1fsum  16487  oddpwp1fsum  16488  bitsfzo  16531  bitsfi  16533  sadcaddlem  16553  smumullem  16588  gcdcl  16602  dvdsgcdidd  16633  mulgcd  16644  rplpwr  16654  rprpwr  16655  rppwr  16656  nn0rppwr  16657  expgcd  16659  lcmcl  16697  lcmgcdnn  16707  lcmfcl  16724  nprmdvds1  16803  rpexp  16819  prmdvdsbc  16823  zsqrtelqelz  16855  phiprmpw  16873  eulerthlem2  16879  eulerth  16880  fermltl  16881  odzcllem  16890  odzdvds  16893  odzphi  16894  prm23lt5  16912  pythagtriplem6  16919  pythagtriplem7  16920  pcprmpw2  16980  dvdsprmpweqle  16984  pcprod  16993  pcfac  16997  pcbc  16998  expnprm  17000  pockthlem  17003  pockthg  17004  prmunb  17012  prmreclem2  17015  prmreclem3  17016  prmreclem4  17017  prmreclem5  17018  prmreclem6  17019  mul4sqlem  17051  4sqlem11  17053  4sqlem17  17059  vdwlem1  17079  vdwlem5  17083  vdwlem6  17084  vdwlem8  17086  vdwlem9  17087  vdwlem11  17089  vdwlem12  17090  vdwnnlem3  17095  ramz2  17122  ramub1lem1  17124  ramub1lem2  17125  ramub1  17126  prmgaplem3  17151  2expltfac  17190  psgnunilem3  19629  odfval  19665  mndodconglem  19674  gexcl3  19720  pgpfi1  19728  sylow1lem1  19731  gexexlem  19985  prmcyg  20027  gsumval3  20040  ablfacrplem  20200  ablfacrp  20201  ablfacrp2  20202  ablfac1eu  20208  prmgrpsimpgd  20249  srgbinomlem3  20373  srgbinomlem4  20374  fermltlchr  21748  freshmansdream  21793  chfacfscmulgsum  23091  chfacfpmmulgsum  23095  cpmadugsumlemF  23107  ovoliunlem1  25736  mbfi1fseqlem1  25949  mbfi1fseqlem3  25951  mbfi1fseqlem5  25953  itg2cnlem2  25996  plyn0mulidp  26518  dvply1  26521  aalioulem2  26576  aalioulem5  26579  aaliou3lem1  26585  aaliou3lem2  26586  aaliou3lem8  26588  aaliou3lem6  26591  taylthlem1  26616  taylthlem2  26617  pserdvlem2  26671  cxpeq  27002  zrtelqelz  27003  dmgmdivn0  27272  lgamgulmlem5  27277  lgamcvg2  27299  wilthlem1  27312  ftalem1  27317  ftalem2  27318  ftalem4  27320  ftalem5  27321  basellem2  27326  basellem3  27327  basellem4  27328  basellem5  27329  isppw2  27359  mpodvdsmulf1o  27438  dvdsmulf1o  27440  sgmmul  27445  fsumvma2  27458  chpchtsum  27463  logfacubnd  27465  mersenne  27471  perfect1  27472  perfectlem1  27473  perfectlem2  27474  perfect  27475  dchrelbas3  27482  dchrelbasd  27483  dchrzrh1  27488  dchrzrhmul  27490  dchrmulcl  27493  dchrn0  27494  dchrfi  27499  dchrghm  27500  dchrabs  27504  dchrinv  27505  dchrptlem1  27508  dchrptlem2  27509  dchrptlem3  27510  dchrpt  27511  dchrsum2  27512  sum2dchr  27518  pcbcctr  27520  bcmono  27521  bclbnd  27524  bposlem1  27528  bposlem3  27530  bposlem5  27532  bposlem6  27533  lgslem1  27541  lgsval2lem  27551  lgsvalmod  27560  lgsmod  27567  lgsdirprm  27575  lgsne0  27579  lgsqrlem1  27590  lgsqrlem2  27591  lgsqrlem3  27592  lgsqrlem4  27593  gausslemma2dlem0b  27601  gausslemma2dlem0c  27602  gausslemma2dlem1  27610  gausslemma2dlem7  27617  gausslemma2d  27618  lgseisenlem1  27619  lgseisenlem2  27620  lgseisenlem3  27621  lgseisenlem4  27622  lgseisen  27623  lgsquadlem2  27625  lgsquadlem3  27626  m1lgs  27632  2lgslem1a  27635  2sqlem3  27664  2sqblem  27675  chebbnd1lem1  27713  chebbnd1lem3  27715  rplogsumlem2  27729  rpvmasumlem  27731  dchrisumlem1  27733  dchrisumlem2  27734  dchrmusum2  27738  dchrvmasumlem3  27743  dchrisum0ff  27751  dchrisum0flblem1  27752  rpvmasum2  27756  dchrisum0re  27757  dchrisum0lem2a  27761  dirith  27773  mudivsum  27774  pntpbnd1a  27829  pntlemq  27845  pntlemr  27846  pntlemj  27847  ostth2lem1  27862  ostth2lem2  27878  ostth2lem3  27879  ostth2  27881  crctcshwlkn0lem6  30291  hashecclwwlkn1  30555  umgrhashecclwwlk  30556  clwwlknon  30568  eucrctshift  30731  numclwlk1lem2  30858  nrt2irr  30961  dipcl  31201  dipcn  31209  bcm1n  33274  expgt0b  33295  nexple  33311  2exple2exp  33312  oexpled  33314  wrdpmtrlast  33541  psgnfzto1st  33553  isarchi2  33633  submarchi  33634  znfermltl  33809  fldextrspundgdvdslem  34198  fldextrspundgdvds  34199  fldext2rspun  34200  constrext2chnlem  34268  cos9thpiminplylem2  34301  submateqlem1  34325  madjusmdetlem2  34346  madjusmdetlem4  34348  mdetlap  34350  oddpwdc  34873  eulerpartlemsv2  34877  eulerpartlemsf  34878  eulerpartlems  34879  eulerpartlemv  34883  eulerpartlemb  34887  signsvtn0  35086  fsum2dsub  35123  reprinfz1  35138  reprpmtf1o  35142  circlemeth  35156  circlemethnat  35157  hgt750lemb  35172  hgt750lema  35173  hgt750leme  35174  tgoldbachgtde  35176  tgoldbachgtda  35177  lpadleft  35202  subfacp1lem1  35766  subfacp1lem6  35772  subfaclim  35775  erdszelem8  35785  erdszelem10  35787  cvmliftlem10  35881  faclim2  36335  poimirlem7  38384  poimirlem17  38394  poimirlem18  38395  poimirlem20  38397  poimirlem21  38398  poimirlem22  38399  poimirlem25  38402  poimirlem26  38403  poimirlem27  38404  poimirlem28  38405  poimirlem32  38409  nninfnub  38509  bfplem1  38580  zndvdchrrhm  42847  lcmineqlem1  42903  lcmineqlem2  42904  lcmineqlem8  42910  lcmineqlem10  42912  lcmineqlem11  42913  lcmineqlem15  42917  lcmineqlem16  42918  lcmineqlem18  42920  lcmineqlem19  42921  lcmineqlem20  42922  lcmineqlem21  42923  lcmineqlem22  42924  3lexlogpow2ineq2  42933  dvrelogpow2b  42942  aks4d1p1p2  42944  aks4d1p1p4  42945  aks4d1p1  42950  aks4d1p3  42952  aks4d1p7d1  42956  aks4d1p7  42957  aks4d1p8  42961  aks4d1p9  42962  isprimroot2  42968  primrootsunit1  42971  primrootscoprmpow  42973  posbezout  42974  primrootscoprbij  42976  primrootlekpowne0  42979  primrootspoweq0  42980  aks6d1c1p2  42983  aks6d1c1p3  42984  aks6d1c1p4  42985  aks6d1c1p5  42986  aks6d1c1p7  42987  aks6d1c1p6  42988  aks6d1c1p8  42989  aks6d1c2p2  42993  hashscontpowcl  42994  hashscontpow1  42995  hashscontpow  42996  aks6d1c4  42998  aks6d1c2lem3  43000  aks6d1c2lem4  43001  aks6d1c2  43004  sticksstones6  43025  sticksstones7  43026  sticksstones10  43029  sticksstones12a  43031  sticksstones12  43032  sticksstones20  43040  sticksstones22  43042  aks6d1c6lem2  43045  aks6d1c6lem3  43046  aks6d1c6lem4  43047  aks6d1c6isolem1  43048  aks6d1c6isolem2  43049  aks6d1c6lem5  43051  bcled  43052  bcle2d  43053  aks6d1c7lem1  43054  aks6d1c7  43058  aks5lem2  43061  aks5lem3a  43063  aks5lem5a  43065  grpods  43068  unitscyglem2  43070  unitscyglem4  43072  aks5lem7  43074  aks5  43078  sumcubes  43196  oexpreposd  43205  exp11d  43209  dvdsexpb  43218  fiabv  43426  fsuppind  43444  dffltz  43488  fltdvdsabdvdsc  43492  fltne  43498  flt4lem4  43503  flt4lem7  43513  fltltc  43515  fltnltalem  43516  fltnlta  43517  3rexfrabdioph  43646  4rexfrabdioph  43647  6rexfrabdioph  43648  7rexfrabdioph  43649  irrapxlem5  43675  pellexlem2  43679  pellexlem6  43683  pell14qrgt0  43708  pell1qrge1  43719  pellfundgt1  43732  ltrmxnn0  43798  jm2.26lem3  43850  jm2.27a  43854  jm2.27c  43856  rmxdiophlem  43864  jm3.1lem1  43866  jm3.1lem2  43867  jm3.1lem3  43868  jm3.1  43869  dgrsub2  43984  mpaaeu  43999  idomsubgmo  44042  relexpxpmin  44565  nzprmdif  45151  binomcxplemwb  45180  fperiodmul  46145  xralrple4  46210  fsumnncl  46410  dvsinexp  46747  dvxpaek  46776  itgsinexplem1  46790  stoweidlem1  46837  stoweidlem17  46853  stoweidlem25  46861  stoweidlem34  46870  stoweidlem38  46874  stoweidlem40  46876  stoweidlem42  46878  stoweidlem45  46881  stirlinglem4  46913  stirlinglem5  46914  stirlinglem10  46919  stirlinglem13  46922  dirkertrigeq  46937  fourierdlem21  46964  fourierdlem25  46968  fourierdlem48  46990  fourierdlem54  46996  fourierdlem64  47006  fourierdlem65  47007  fourierdlem73  47015  fourierdlem81  47023  fourierdlem83  47025  fourierdlem92  47034  fourierdlem103  47045  fourierdlem104  47046  fourierdlem112  47054  fourierdlem113  47055  etransclem1  47071  etransclem4  47074  etransclem8  47078  etransclem15  47085  etransclem17  47087  etransclem18  47088  etransclem19  47089  etransclem20  47090  etransclem21  47091  etransclem22  47092  etransclem23  47093  etransclem24  47094  etransclem25  47095  etransclem27  47097  etransclem32  47102  etransclem35  47105  etransclem41  47111  etransclem44  47114  etransclem46  47116  modmknepk  48264  iccpartigtl  48331  iccpartgt  48335  iccpartgel  48337  iccelpart  48341  odz2prm2pw  48474  fmtnoprmfac1  48476  fmtnoprmfac2  48478  2pwp1prm  48500  sfprmdvdsmersenne  48514  lighneallem4a  48519  proththdlem  48524  proththd  48525  perfectALTVlem1  48645  perfectALTVlem2  48646  perfectALTV  48647  fpprwpprb  48664  gpgedgvtx1  48986  logbpw2m1  49505  nnpw2blenfzo  49519  nnolog2flm1  49528  dignn0fr  49539  nn0sumshdiglemA  49557  nn0sumshdiglemB  49558