Theorem nnnn0d 12660

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

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

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-n0 12600

This theorem is used by:  nn0ge2m1nn0  12670  nnzd  12712  eluzge2nn0  13012  expgt1  14236  expaddzlem  14241  expaddz  14242  expmulz  14244  expmulnbnd  14372  exp11nnd  14398  facwordi  14426  faclbnd  14427  facavg  14438  bcm1k  14452  wrdeqs1cat  14862  cshwcsh2id  14972  relexpsucnnr  15171  isercolllem2  15826  bcxmas  15997  climcndslem1  16011  climcndslem2  16012  climcnds  16013  pwdif  16030  geo2sum  16035  mertenslem1  16046  prodmolem3  16093  prodmolem2a  16094  bpolydiflem  16213  eftabs  16234  efcllem  16236  eftlub  16270  eirrlem  16365  rpnnen2lem9  16383  rpnnen2lem11  16385  dvdsfac  16489  pwp1fsum  16554  oddpwp1fsum  16555  bitsfzo  16598  bitsfi  16600  sadcaddlem  16620  smumullem  16655  gcdcl  16669  dvdsgcdidd  16703  mulgcd  16714  rplpwr  16725  rprpwr  16726  rppwr  16727  nn0rppwr  16728  expgcd  16730  lcmcl  16769  lcmgcdnn  16779  lcmfcl  16796  nprmdvds1  16875  rpexp  16891  prmdvdsbc  16895  zsqrtelqelz  16927  phiprmpw  16946  eulerthlem2  16952  eulerth  16953  fermltl  16954  odzcllem  16963  odzdvds  16966  odzphi  16967  prm23lt5  16985  pythagtriplem6  16992  pythagtriplem7  16993  pcprmpw2  17053  dvdsprmpweqle  17057  pcprod  17066  pcfac  17070  pcbc  17071  expnprm  17073  pockthlem  17076  pockthg  17077  prmunb  17085  prmreclem2  17088  prmreclem3  17089  prmreclem4  17090  prmreclem5  17091  prmreclem6  17092  mul4sqlem  17124  4sqlem11  17126  4sqlem17  17132  vdwlem1  17152  vdwlem5  17156  vdwlem6  17157  vdwlem8  17159  vdwlem9  17160  vdwlem11  17162  vdwlem12  17163  vdwnnlem3  17168  ramz2  17195  ramub1lem1  17197  ramub1lem2  17198  ramub1  17199  prmgaplem3  17224  2expltfac  17263  psgnunilem3  19703  odfval  19739  mndodconglem  19748  gexcl3  19794  pgpfi1  19802  sylow1lem1  19805  gexexlem  20059  prmcyg  20101  gsumval3  20114  ablfacrplem  20274  ablfacrp  20275  ablfacrp2  20276  ablfac1eu  20282  prmgrpsimpgd  20323  srgbinomlem3  20447  srgbinomlem4  20448  fermltlchr  21828  freshmansdream  21873  chfacfscmulgsum  23171  chfacfpmmulgsum  23175  cpmadugsumlemF  23187  ovoliunlem1  25816  mbfi1fseqlem1  26029  mbfi1fseqlem3  26031  mbfi1fseqlem5  26033  itg2cnlem2  26076  plyn0mulidp  26595  dvply1  26598  aalioulem2  26653  aalioulem5  26656  aaliou3lem1  26662  aaliou3lem2  26663  aaliou3lem8  26665  aaliou3lem6  26668  taylthlem1  26693  taylthlem2  26694  pserdvlem2  26748  cxpeq  27078  zrtelqelz  27079  dmgmdivn0  27348  lgamgulmlem5  27353  lgamcvg2  27375  wilthlem1  27388  ftalem1  27393  ftalem2  27394  ftalem4  27396  ftalem5  27397  basellem2  27402  basellem3  27403  basellem4  27404  basellem5  27405  isppw2  27435  mpodvdsmulf1o  27514  dvdsmulf1o  27516  sgmmul  27521  fsumvma2  27534  chpchtsum  27539  logfacubnd  27541  mersenne  27547  perfect1  27548  perfectlem1  27549  perfectlem2  27550  perfect  27551  dchrelbas3  27558  dchrelbasd  27559  dchrzrh1  27564  dchrzrhmul  27566  dchrmulcl  27569  dchrn0  27570  dchrfi  27575  dchrghm  27576  dchrabs  27580  dchrinv  27581  dchrptlem1  27584  dchrptlem2  27585  dchrptlem3  27586  dchrpt  27587  dchrsum2  27588  sum2dchr  27594  pcbcctr  27596  bcmono  27597  bclbnd  27600  bposlem1  27604  bposlem3  27606  bposlem5  27608  bposlem6  27609  lgslem1  27617  lgsval2lem  27627  lgsvalmod  27636  lgsmod  27643  lgsdirprm  27651  lgsne0  27655  lgsqrlem1  27666  lgsqrlem2  27667  lgsqrlem3  27668  lgsqrlem4  27669  gausslemma2dlem0b  27677  gausslemma2dlem0c  27678  gausslemma2dlem1  27686  gausslemma2dlem7  27693  gausslemma2d  27694  lgseisenlem1  27695  lgseisenlem2  27696  lgseisenlem3  27697  lgseisenlem4  27698  lgseisen  27699  lgsquadlem2  27701  lgsquadlem3  27702  m1lgs  27708  2lgslem1a  27711  2sqlem3  27740  2sqblem  27751  chebbnd1lem1  27789  chebbnd1lem3  27791  rplogsumlem2  27805  rpvmasumlem  27807  dchrisumlem1  27809  dchrisumlem2  27810  dchrmusum2  27814  dchrvmasumlem3  27819  dchrisum0ff  27827  dchrisum0flblem1  27828  rpvmasum2  27832  dchrisum0re  27833  dchrisum0lem2a  27837  dirith  27849  mudivsum  27850  pntpbnd1a  27905  pntlemq  27921  pntlemr  27922  pntlemj  27923  ostth2lem1  27938  ostth2lem2  27954  ostth2lem3  27955  ostth2  27957  fltdvdsabdvdsc  27963  fltne  27968  flt4lem4  27972  flt4lem7  27982  fltoprm  27988  crctcshwlkn0lem6  30397  hashecclwwlkn1  30661  umgrhashecclwwlk  30662  clwwlknon  30674  eucrctshift  30837  numclwlk1lem2  30964  nrt2irr  31067  dipcl  31307  dipcn  31315  bcm1n  33380  expgt0b  33401  nexple  33417  2exple2exp  33418  oexpled  33420  wrdpmtrlast  33647  psgnfzto1st  33659  isarchi2  33739  submarchi  33740  znfermltl  33915  fldextrspundgdvdslem  34305  fldextrspundgdvds  34306  fldext2rspun  34307  constrext2chnlem  34375  cos9thpiminplylem2  34408  submateqlem1  34432  madjusmdetlem2  34453  madjusmdetlem4  34455  mdetlap  34457  oddpwdc  34979  eulerpartlemsv2  34983  eulerpartlemsf  34984  eulerpartlems  34985  eulerpartlemv  34989  eulerpartlemb  34993  signsvtn0  35192  fsum2dsub  35229  reprinfz1  35244  reprpmtf1o  35248  circlemeth  35262  circlemethnat  35263  hgt750lemb  35278  hgt750lema  35279  hgt750leme  35280  tgoldbachgtde  35282  tgoldbachgtda  35283  lpadleft  35308  subfacp1lem1  35923  subfacp1lem6  35929  subfaclim  35932  erdszelem8  35942  erdszelem10  35944  cvmliftlem10  36038  faclim2  36492  poimirlem7  38525  poimirlem17  38535  poimirlem18  38536  poimirlem20  38538  poimirlem21  38539  poimirlem22  38540  poimirlem25  38543  poimirlem26  38544  poimirlem27  38545  poimirlem28  38546  poimirlem32  38550  nninfnub  38665  bfplem1  38736  zndvdchrrhm  43003  lcmineqlem1  43059  lcmineqlem2  43060  lcmineqlem8  43066  lcmineqlem10  43068  lcmineqlem11  43069  lcmineqlem15  43073  lcmineqlem16  43074  lcmineqlem18  43076  lcmineqlem19  43077  lcmineqlem20  43078  lcmineqlem21  43079  lcmineqlem22  43080  3lexlogpow2ineq2  43089  dvrelogpow2b  43098  aks4d1p1p2  43100  aks4d1p1p4  43101  aks4d1p1  43106  aks4d1p3  43108  aks4d1p7d1  43112  aks4d1p7  43113  aks4d1p8  43117  aks4d1p9  43118  isprimroot2  43124  primrootsunit1  43127  primrootscoprmpow  43129  posbezout  43130  primrootscoprbij  43132  primrootlekpowne0  43135  primrootspoweq0  43136  aks6d1c1p2  43139  aks6d1c1p3  43140  aks6d1c1p4  43141  aks6d1c1p5  43142  aks6d1c1p7  43143  aks6d1c1p6  43144  aks6d1c1p8  43145  aks6d1c2p2  43149  hashscontpowcl  43150  hashscontpow1  43151  hashscontpow  43152  aks6d1c4  43154  aks6d1c2lem3  43156  aks6d1c2lem4  43157  aks6d1c2  43160  sticksstones6  43181  sticksstones7  43182  sticksstones10  43185  sticksstones12a  43187  sticksstones12  43188  sticksstones20  43196  sticksstones22  43198  aks6d1c6lem2  43201  aks6d1c6lem3  43202  aks6d1c6lem4  43203  aks6d1c6isolem1  43204  aks6d1c6isolem2  43205  aks6d1c6lem5  43207  bcled  43208  bcle2d  43209  aks6d1c7lem1  43210  aks6d1c7  43214  aks5lem2  43217  aks5lem3a  43219  aks5lem5a  43221  grpods  43224  unitscyglem2  43226  unitscyglem4  43228  aks5lem7  43230  aks5  43234  sumcubes  43350  oexpreposd  43359  exp11d  43363  dvdsexpb  43367  fiabv  43580  fsuppind  43598  dffltz  43650  fltltc  43652  fltnltalem  43653  fltnlta  43654  3rexfrabdioph  43783  4rexfrabdioph  43784  6rexfrabdioph  43785  7rexfrabdioph  43786  irrapxlem5  43812  pellexlem2  43816  pellexlem6  43820  pell14qrgt0  43845  pell1qrge1  43856  pellfundgt1  43869  ltrmxnn0  43935  jm2.26lem3  43987  jm2.27a  43991  jm2.27c  43993  rmxdiophlem  44001  jm3.1lem1  44003  jm3.1lem2  44004  jm3.1lem3  44005  jm3.1  44006  dgrsub2  44121  mpaaeu  44136  idomsubgmo  44179  relexpxpmin  44702  nzprmdif  45288  binomcxplemwb  45317  fperiodmul  46289  xralrple4  46353  fsumnncl  46553  dvsinexp  46890  dvxpaek  46919  itgsinexplem1  46933  stoweidlem1  46980  stoweidlem17  46996  stoweidlem25  47004  stoweidlem34  47013  stoweidlem38  47017  stoweidlem40  47019  stoweidlem42  47021  stoweidlem45  47024  stirlinglem4  47056  stirlinglem5  47057  stirlinglem10  47062  stirlinglem13  47065  dirkertrigeq  47080  fourierdlem21  47107  fourierdlem25  47111  fourierdlem48  47133  fourierdlem54  47139  fourierdlem64  47149  fourierdlem65  47150  fourierdlem73  47158  fourierdlem81  47166  fourierdlem83  47168  fourierdlem92  47177  fourierdlem103  47188  fourierdlem104  47189  fourierdlem112  47197  fourierdlem113  47198  etransclem1  47214  etransclem4  47217  etransclem8  47221  etransclem15  47228  etransclem17  47230  etransclem18  47231  etransclem19  47232  etransclem20  47233  etransclem21  47234  etransclem22  47235  etransclem23  47236  etransclem24  47237  etransclem25  47238  etransclem27  47240  etransclem32  47245  etransclem35  47248  etransclem41  47254  etransclem44  47257  etransclem46  47259  modmknepk  48407  iccpartigtl  48474  iccpartgt  48478  iccpartgel  48480  iccelpart  48484  odz2prm2pw  48617  fmtnoprmfac1  48619  fmtnoprmfac2  48621  2pwp1prm  48643  sfprmdvdsmersenne  48657  lighneallem4a  48662  proththdlem  48667  proththd  48668  perfectALTVlem1  48788  perfectALTVlem2  48789  perfectALTV  48790  fpprwpprb  48807  gpgedgvtx1  49129  logbpw2m1  49648  nnpw2blenfzo  49662  nnolog2flm1  49671  dignn0fr  49682  nn0sumshdiglemA  49700  nn0sumshdiglemB  49701