Theorem nnnn0d 12474

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕcn 12157  ℕ₀cn0 12413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-n0 12414

This theorem is referenced by:  nn0ge2m1nn0  12484  nnzd  12526  eluzge2nn0  12817  expgt1  14035  expaddzlem  14040  expaddz  14041  expmulz  14043  expmulnbnd  14170  exp11nnd  14196  facwordi  14224  faclbnd  14225  facavg  14236  bcm1k  14250  wrdeqs1cat  14655  cshwcsh2id  14763  relexpsucnnr  14960  isercolllem2  15601  bcxmas  15770  climcndslem1  15784  climcndslem2  15785  climcnds  15786  pwdif  15803  geo2sum  15808  mertenslem1  15819  prodmolem3  15868  prodmolem2a  15869  bpolydiflem  15989  eftabs  16010  efcllem  16012  eftlub  16046  eirrlem  16141  rpnnen2lem9  16159  rpnnen2lem11  16161  dvdsfac  16265  pwp1fsum  16330  oddpwp1fsum  16331  bitsfzo  16374  bitsfi  16376  sadcaddlem  16396  smumullem  16431  gcdcl  16445  dvdsgcdidd  16476  mulgcd  16487  rplpwr  16497  rprpwr  16498  rppwr  16499  nn0rppwr  16500  expgcd  16502  lcmcl  16540  lcmgcdnn  16550  lcmfcl  16567  nprmdvds1  16645  rpexp  16661  prmdvdsbc  16665  zsqrtelqelz  16697  phiprmpw  16715  eulerthlem2  16721  eulerth  16722  fermltl  16723  odzcllem  16732  odzdvds  16735  odzphi  16736  prm23lt5  16754  pythagtriplem6  16761  pythagtriplem7  16762  pcprmpw2  16822  dvdsprmpweqle  16826  pcprod  16835  pcfac  16839  pcbc  16840  expnprm  16842  pockthlem  16845  pockthg  16846  prmunb  16854  prmreclem2  16857  prmreclem3  16858  prmreclem4  16859  prmreclem5  16860  prmreclem6  16861  mul4sqlem  16893  4sqlem11  16895  4sqlem17  16901  vdwlem1  16921  vdwlem5  16925  vdwlem6  16926  vdwlem8  16928  vdwlem9  16929  vdwlem11  16931  vdwlem12  16932  vdwnnlem3  16937  ramz2  16964  ramub1lem1  16966  ramub1lem2  16967  ramub1  16968  prmgaplem3  16993  2expltfac  17032  psgnunilem3  19437  odfval  19473  mndodconglem  19482  gexcl3  19528  pgpfi1  19536  sylow1lem1  19539  gexexlem  19793  prmcyg  19835  gsumval3  19848  ablfacrplem  20008  ablfacrp  20009  ablfacrp2  20010  ablfac1eu  20016  prmgrpsimpgd  20057  srgbinomlem3  20175  srgbinomlem4  20176  fermltlchr  21496  freshmansdream  21541  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  cpmadugsumlemF  22832  ovoliunlem1  25471  mbfi1fseqlem1  25684  mbfi1fseqlem3  25686  mbfi1fseqlem5  25688  itg2cnlem2  25731  dvply1  26259  aalioulem2  26309  aalioulem5  26312  aaliou3lem1  26318  aaliou3lem2  26319  aaliou3lem8  26321  aaliou3lem6  26324  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  pserdvlem2  26406  cxpeq  26735  zrtelqelz  26736  dmgmdivn0  27006  lgamgulmlem5  27011  lgamcvg2  27033  wilthlem1  27046  ftalem1  27051  ftalem2  27052  ftalem4  27054  ftalem5  27055  basellem2  27060  basellem3  27061  basellem4  27062  basellem5  27063  isppw2  27093  mpodvdsmulf1o  27172  dvdsmulf1o  27174  sgmmul  27180  fsumvma2  27193  chpchtsum  27198  logfacubnd  27200  mersenne  27206  perfect1  27207  perfectlem1  27208  perfectlem2  27209  perfect  27210  dchrelbas3  27217  dchrelbasd  27218  dchrzrh1  27223  dchrzrhmul  27225  dchrmulcl  27228  dchrn0  27229  dchrfi  27234  dchrghm  27235  dchrabs  27239  dchrinv  27240  dchrptlem1  27243  dchrptlem2  27244  dchrptlem3  27245  dchrpt  27246  dchrsum2  27247  sum2dchr  27253  pcbcctr  27255  bcmono  27256  bclbnd  27259  bposlem1  27263  bposlem3  27265  bposlem5  27267  bposlem6  27268  lgslem1  27276  lgsval2lem  27286  lgsvalmod  27295  lgsmod  27302  lgsdirprm  27310  lgsne0  27314  lgsqrlem1  27325  lgsqrlem2  27326  lgsqrlem3  27327  lgsqrlem4  27328  gausslemma2dlem0b  27336  gausslemma2dlem0c  27337  gausslemma2dlem1  27345  gausslemma2dlem7  27352  gausslemma2d  27353  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem3  27356  lgseisenlem4  27357  lgseisen  27358  lgsquadlem2  27360  lgsquadlem3  27361  m1lgs  27367  2lgslem1a  27370  2sqlem3  27399  2sqblem  27410  chebbnd1lem1  27448  chebbnd1lem3  27450  rplogsumlem2  27464  rpvmasumlem  27466  dchrisumlem1  27468  dchrisumlem2  27469  dchrmusum2  27473  dchrvmasumlem3  27478  dchrisum0ff  27486  dchrisum0flblem1  27487  rpvmasum2  27491  dchrisum0re  27492  dchrisum0lem2a  27496  dirith  27508  mudivsum  27509  pntpbnd1a  27564  pntlemq  27580  pntlemr  27581  pntlemj  27582  ostth2lem1  27597  ostth2lem2  27613  ostth2lem3  27614  ostth2  27616  crctcshwlkn0lem6  29900  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  clwwlknon  30177  eucrctshift  30330  numclwlk1lem2  30457  nrt2irr  30560  dipcl  30800  dipcn  30808  bcm1n  32886  expgt0b  32908  nexple  32936  2exple2exp  32937  oexpled  32939  wrdpmtrlast  33187  psgnfzto1st  33199  isarchi2  33279  submarchi  33280  znfermltl  33459  fldextrspundgdvdslem  33858  fldextrspundgdvds  33859  fldext2rspun  33860  constrext2chnlem  33928  cos9thpiminplylem2  33961  submateqlem1  33985  madjusmdetlem2  34006  madjusmdetlem4  34008  mdetlap  34010  oddpwdc  34532  eulerpartlemsv2  34536  eulerpartlemsf  34537  eulerpartlems  34538  eulerpartlemv  34542  eulerpartlemb  34546  plymulx0  34725  signsvtn0  34748  fsum2dsub  34785  reprinfz1  34800  reprpmtf1o  34804  circlemeth  34818  circlemethnat  34819  hgt750lemb  34834  hgt750lema  34835  hgt750leme  34836  tgoldbachgtde  34838  tgoldbachgtda  34839  lpadleft  34861  subfacp1lem1  35395  subfacp1lem6  35401  subfaclim  35404  erdszelem8  35414  erdszelem10  35416  cvmliftlem10  35510  faclim2  35964  poimirlem7  37878  poimirlem17  37888  poimirlem18  37889  poimirlem20  37891  poimirlem21  37892  poimirlem22  37893  poimirlem25  37896  poimirlem26  37897  poimirlem27  37898  poimirlem28  37899  poimirlem32  37903  nninfnub  38002  bfplem1  38073  zndvdchrrhm  42342  lcmineqlem1  42399  lcmineqlem2  42400  lcmineqlem8  42406  lcmineqlem10  42408  lcmineqlem11  42409  lcmineqlem15  42413  lcmineqlem16  42414  lcmineqlem18  42416  lcmineqlem19  42417  lcmineqlem20  42418  lcmineqlem21  42419  lcmineqlem22  42420  3lexlogpow2ineq2  42429  dvrelogpow2b  42438  aks4d1p1p2  42440  aks4d1p1p4  42441  aks4d1p1  42446  aks4d1p3  42448  aks4d1p7d1  42452  aks4d1p7  42453  aks4d1p8  42457  aks4d1p9  42458  isprimroot2  42464  primrootsunit1  42467  primrootscoprmpow  42469  posbezout  42470  primrootscoprbij  42472  primrootlekpowne0  42475  primrootspoweq0  42476  aks6d1c1p2  42479  aks6d1c1p3  42480  aks6d1c1p4  42481  aks6d1c1p5  42482  aks6d1c1p7  42483  aks6d1c1p6  42484  aks6d1c1p8  42485  aks6d1c2p2  42489  hashscontpowcl  42490  hashscontpow1  42491  hashscontpow  42492  aks6d1c4  42494  aks6d1c2lem3  42496  aks6d1c2lem4  42497  aks6d1c2  42500  sticksstones6  42521  sticksstones7  42522  sticksstones10  42525  sticksstones12a  42527  sticksstones12  42528  sticksstones20  42536  sticksstones22  42538  aks6d1c6lem2  42541  aks6d1c6lem3  42542  aks6d1c6lem4  42543  aks6d1c6isolem1  42544  aks6d1c6isolem2  42545  aks6d1c6lem5  42547  bcled  42548  bcle2d  42549  aks6d1c7lem1  42550  aks6d1c7  42554  aks5lem2  42557  aks5lem3a  42559  aks5lem5a  42561  grpods  42564  unitscyglem2  42566  unitscyglem4  42568  aks5lem7  42570  aks5  42574  sumcubes  42683  oexpreposd  42692  exp11d  42696  dvdsexpb  42705  fiabv  42906  fsuppind  42948  dffltz  42992  fltdvdsabdvdsc  42996  fltne  43002  flt4lem4  43007  flt4lem7  43017  fltltc  43019  fltnltalem  43020  fltnlta  43021  3rexfrabdioph  43154  4rexfrabdioph  43155  6rexfrabdioph  43156  7rexfrabdioph  43157  irrapxlem5  43183  pellexlem2  43187  pellexlem6  43191  pell14qrgt0  43216  pell1qrge1  43227  pellfundgt1  43240  ltrmxnn0  43306  jm2.26lem3  43358  jm2.27a  43362  jm2.27c  43364  rmxdiophlem  43372  jm3.1lem1  43374  jm3.1lem2  43375  jm3.1lem3  43376  jm3.1  43377  dgrsub2  43492  mpaaeu  43507  idomsubgmo  43550  relexpxpmin  44073  nzprmdif  44675  binomcxplemwb  44704  fperiodmul  45666  xralrple4  45731  fsumnncl  45932  dvsinexp  46269  dvxpaek  46298  itgsinexplem1  46312  stoweidlem1  46359  stoweidlem17  46375  stoweidlem25  46383  stoweidlem34  46392  stoweidlem38  46396  stoweidlem40  46398  stoweidlem42  46400  stoweidlem45  46403  stirlinglem4  46435  stirlinglem5  46436  stirlinglem10  46441  stirlinglem13  46444  dirkertrigeq  46459  fourierdlem21  46486  fourierdlem25  46490  fourierdlem48  46512  fourierdlem54  46518  fourierdlem64  46528  fourierdlem65  46529  fourierdlem73  46537  fourierdlem81  46545  fourierdlem83  46547  fourierdlem92  46556  fourierdlem103  46567  fourierdlem104  46568  fourierdlem112  46576  fourierdlem113  46577  etransclem1  46593  etransclem4  46596  etransclem8  46600  etransclem15  46607  etransclem17  46609  etransclem18  46610  etransclem19  46611  etransclem20  46612  etransclem21  46613  etransclem22  46614  etransclem23  46615  etransclem24  46616  etransclem25  46617  etransclem27  46619  etransclem32  46624  etransclem35  46627  etransclem41  46633  etransclem44  46636  etransclem46  46638  modmknepk  47722  iccpartigtl  47783  iccpartgt  47787  iccpartgel  47789  iccelpart  47793  odz2prm2pw  47923  fmtnoprmfac1  47925  fmtnoprmfac2  47927  2pwp1prm  47949  sfprmdvdsmersenne  47963  lighneallem4a  47968  proththdlem  47973  proththd  47974  perfectALTVlem1  48081  perfectALTVlem2  48082  perfectALTV  48083  fpprwpprb  48100  gpgedgvtx1  48422  logbpw2m1  48927  nnpw2blenfzo  48941  nnolog2flm1  48950  dignn0fr  48961  nn0sumshdiglemA  48979  nn0sumshdiglemB  48980