Theorem nnnn0d 12479

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℕcn 12162  ℕ₀cn0 12418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-ss 3928  df-n0 12419

This theorem is referenced by:  nn0ge2m1nn0  12489  nnzd  12532  eluzge2nn0  12827  expgt1  14041  expaddzlem  14046  expaddz  14047  expmulz  14049  expmulnbnd  14176  exp11nnd  14202  facwordi  14230  faclbnd  14231  facavg  14242  bcm1k  14256  wrdeqs1cat  14661  cshwcsh2id  14770  relexpsucnnr  14967  isercolllem2  15608  bcxmas  15777  climcndslem1  15791  climcndslem2  15792  climcnds  15793  pwdif  15810  geo2sum  15815  mertenslem1  15826  prodmolem3  15875  prodmolem2a  15876  bpolydiflem  15996  eftabs  16017  efcllem  16019  eftlub  16053  eirrlem  16148  rpnnen2lem9  16166  rpnnen2lem11  16168  dvdsfac  16272  pwp1fsum  16337  oddpwp1fsum  16338  bitsfzo  16381  bitsfi  16383  sadcaddlem  16403  smumullem  16438  gcdcl  16452  dvdsgcdidd  16483  mulgcd  16494  rplpwr  16504  rprpwr  16505  rppwr  16506  nn0rppwr  16507  expgcd  16509  lcmcl  16547  lcmgcdnn  16557  lcmfcl  16574  nprmdvds1  16652  rpexp  16668  prmdvdsbc  16672  zsqrtelqelz  16704  phiprmpw  16722  eulerthlem2  16728  eulerth  16729  fermltl  16730  odzcllem  16739  odzdvds  16742  odzphi  16743  prm23lt5  16761  pythagtriplem6  16768  pythagtriplem7  16769  pcprmpw2  16829  dvdsprmpweqle  16833  pcprod  16842  pcfac  16846  pcbc  16847  expnprm  16849  pockthlem  16852  pockthg  16853  prmunb  16861  prmreclem2  16864  prmreclem3  16865  prmreclem4  16866  prmreclem5  16867  prmreclem6  16868  mul4sqlem  16900  4sqlem11  16902  4sqlem17  16908  vdwlem1  16928  vdwlem5  16932  vdwlem6  16933  vdwlem8  16935  vdwlem9  16936  vdwlem11  16938  vdwlem12  16939  vdwnnlem3  16944  ramz2  16971  ramub1lem1  16973  ramub1lem2  16974  ramub1  16975  prmgaplem3  17000  2expltfac  17039  psgnunilem3  19402  odfval  19438  mndodconglem  19447  gexcl3  19493  pgpfi1  19501  sylow1lem1  19504  gexexlem  19758  prmcyg  19800  gsumval3  19813  ablfacrplem  19973  ablfacrp  19974  ablfacrp2  19975  ablfac1eu  19981  prmgrpsimpgd  20022  srgbinomlem3  20113  srgbinomlem4  20114  fermltlchr  21415  freshmansdream  21460  chfacfscmulgsum  22723  chfacfpmmulgsum  22727  cpmadugsumlemF  22739  ovoliunlem1  25379  mbfi1fseqlem1  25592  mbfi1fseqlem3  25594  mbfi1fseqlem5  25596  itg2cnlem2  25639  dvply1  26167  aalioulem2  26217  aalioulem5  26220  aaliou3lem1  26226  aaliou3lem2  26227  aaliou3lem8  26229  aaliou3lem6  26232  taylthlem1  26257  taylthlem2  26258  taylthlem2OLD  26259  pserdvlem2  26314  cxpeq  26643  zrtelqelz  26644  dmgmdivn0  26914  lgamgulmlem5  26919  lgamcvg2  26941  wilthlem1  26954  ftalem1  26959  ftalem2  26960  ftalem4  26962  ftalem5  26963  basellem2  26968  basellem3  26969  basellem4  26970  basellem5  26971  isppw2  27001  mpodvdsmulf1o  27080  dvdsmulf1o  27082  sgmmul  27088  fsumvma2  27101  chpchtsum  27106  logfacubnd  27108  mersenne  27114  perfect1  27115  perfectlem1  27116  perfectlem2  27117  perfect  27118  dchrelbas3  27125  dchrelbasd  27126  dchrzrh1  27131  dchrzrhmul  27133  dchrmulcl  27136  dchrn0  27137  dchrfi  27142  dchrghm  27143  dchrabs  27147  dchrinv  27148  dchrptlem1  27151  dchrptlem2  27152  dchrptlem3  27153  dchrpt  27154  dchrsum2  27155  sum2dchr  27161  pcbcctr  27163  bcmono  27164  bclbnd  27167  bposlem1  27171  bposlem3  27173  bposlem5  27175  bposlem6  27176  lgslem1  27184  lgsval2lem  27194  lgsvalmod  27203  lgsmod  27210  lgsdirprm  27218  lgsne0  27222  lgsqrlem1  27233  lgsqrlem2  27234  lgsqrlem3  27235  lgsqrlem4  27236  gausslemma2dlem0b  27244  gausslemma2dlem0c  27245  gausslemma2dlem1  27253  gausslemma2dlem7  27260  gausslemma2d  27261  lgseisenlem1  27262  lgseisenlem2  27263  lgseisenlem3  27264  lgseisenlem4  27265  lgseisen  27266  lgsquadlem2  27268  lgsquadlem3  27269  m1lgs  27275  2lgslem1a  27278  2sqlem3  27307  2sqblem  27318  chebbnd1lem1  27356  chebbnd1lem3  27358  rplogsumlem2  27372  rpvmasumlem  27374  dchrisumlem1  27376  dchrisumlem2  27377  dchrmusum2  27381  dchrvmasumlem3  27386  dchrisum0ff  27394  dchrisum0flblem1  27395  rpvmasum2  27399  dchrisum0re  27400  dchrisum0lem2a  27404  dirith  27416  mudivsum  27417  pntpbnd1a  27472  pntlemq  27488  pntlemr  27489  pntlemj  27490  ostth2lem1  27505  ostth2lem2  27521  ostth2lem3  27522  ostth2  27524  crctcshwlkn0lem6  29718  hashecclwwlkn1  29979  umgrhashecclwwlk  29980  clwwlknon  29992  eucrctshift  30145  numclwlk1lem2  30272  nrt2irr  30375  dipcl  30614  dipcn  30622  bcm1n  32691  expgt0b  32714  nexple  32742  2exple2exp  32743  oexpled  32745  wrdpmtrlast  33023  psgnfzto1st  33035  isarchi2  33112  submarchi  33113  znfermltl  33310  fldextrspundgdvdslem  33648  fldextrspundgdvds  33649  fldext2rspun  33650  constrext2chnlem  33713  cos9thpiminplylem2  33746  submateqlem1  33770  madjusmdetlem2  33791  madjusmdetlem4  33793  mdetlap  33795  oddpwdc  34318  eulerpartlemsv2  34322  eulerpartlemsf  34323  eulerpartlems  34324  eulerpartlemv  34328  eulerpartlemb  34332  plymulx0  34511  signsvtn0  34534  fsum2dsub  34571  reprinfz1  34586  reprpmtf1o  34590  circlemeth  34604  circlemethnat  34605  hgt750lemb  34620  hgt750lema  34621  hgt750leme  34622  tgoldbachgtde  34624  tgoldbachgtda  34625  lpadleft  34647  subfacp1lem1  35139  subfacp1lem6  35145  subfaclim  35148  erdszelem8  35158  erdszelem10  35160  cvmliftlem10  35254  faclim2  35708  poimirlem7  37594  poimirlem17  37604  poimirlem18  37605  poimirlem20  37607  poimirlem21  37608  poimirlem22  37609  poimirlem25  37612  poimirlem26  37613  poimirlem27  37614  poimirlem28  37615  poimirlem32  37619  nninfnub  37718  bfplem1  37789  zndvdchrrhm  41933  lcmineqlem1  41990  lcmineqlem2  41991  lcmineqlem8  41997  lcmineqlem10  41999  lcmineqlem11  42000  lcmineqlem15  42004  lcmineqlem16  42005  lcmineqlem18  42007  lcmineqlem19  42008  lcmineqlem20  42009  lcmineqlem21  42010  lcmineqlem22  42011  3lexlogpow2ineq2  42020  dvrelogpow2b  42029  aks4d1p1p2  42031  aks4d1p1p4  42032  aks4d1p1  42037  aks4d1p3  42039  aks4d1p7d1  42043  aks4d1p7  42044  aks4d1p8  42048  aks4d1p9  42049  isprimroot2  42055  primrootsunit1  42058  primrootscoprmpow  42060  posbezout  42061  primrootscoprbij  42063  primrootlekpowne0  42066  primrootspoweq0  42067  aks6d1c1p2  42070  aks6d1c1p3  42071  aks6d1c1p4  42072  aks6d1c1p5  42073  aks6d1c1p7  42074  aks6d1c1p6  42075  aks6d1c1p8  42076  aks6d1c2p2  42080  hashscontpowcl  42081  hashscontpow1  42082  hashscontpow  42083  aks6d1c4  42085  aks6d1c2lem3  42087  aks6d1c2lem4  42088  aks6d1c2  42091  sticksstones6  42112  sticksstones7  42113  sticksstones10  42116  sticksstones12a  42118  sticksstones12  42119  sticksstones20  42127  sticksstones22  42129  aks6d1c6lem2  42132  aks6d1c6lem3  42133  aks6d1c6lem4  42134  aks6d1c6isolem1  42135  aks6d1c6isolem2  42136  aks6d1c6lem5  42138  bcled  42139  bcle2d  42140  aks6d1c7lem1  42141  aks6d1c7  42145  aks5lem2  42148  aks5lem3a  42150  aks5lem5a  42152  grpods  42155  unitscyglem2  42157  unitscyglem4  42159  aks5lem7  42161  aks5  42165  sumcubes  42274  oexpreposd  42283  exp11d  42287  dvdsexpb  42296  fiabv  42497  fsuppind  42551  dffltz  42595  fltdvdsabdvdsc  42599  fltne  42605  flt4lem4  42610  flt4lem7  42620  fltltc  42622  fltnltalem  42623  fltnlta  42624  3rexfrabdioph  42758  4rexfrabdioph  42759  6rexfrabdioph  42760  7rexfrabdioph  42761  irrapxlem5  42787  pellexlem2  42791  pellexlem6  42795  pell14qrgt0  42820  pell1qrge1  42831  pellfundgt1  42844  ltrmxnn0  42911  jm2.26lem3  42963  jm2.27a  42967  jm2.27c  42969  rmxdiophlem  42977  jm3.1lem1  42979  jm3.1lem2  42980  jm3.1lem3  42981  jm3.1  42982  dgrsub2  43097  mpaaeu  43112  idomsubgmo  43155  relexpxpmin  43679  nzprmdif  44281  binomcxplemwb  44310  fperiodmul  45275  xralrple4  45342  fsumnncl  45543  dvsinexp  45882  dvxpaek  45911  itgsinexplem1  45925  stoweidlem1  45972  stoweidlem17  45988  stoweidlem25  45996  stoweidlem34  46005  stoweidlem38  46009  stoweidlem40  46011  stoweidlem42  46013  stoweidlem45  46016  stirlinglem4  46048  stirlinglem5  46049  stirlinglem10  46054  stirlinglem13  46057  dirkertrigeq  46072  fourierdlem21  46099  fourierdlem25  46103  fourierdlem48  46125  fourierdlem54  46131  fourierdlem64  46141  fourierdlem65  46142  fourierdlem73  46150  fourierdlem81  46158  fourierdlem83  46160  fourierdlem92  46169  fourierdlem103  46180  fourierdlem104  46181  fourierdlem112  46189  fourierdlem113  46190  etransclem1  46206  etransclem4  46209  etransclem8  46213  etransclem15  46220  etransclem17  46222  etransclem18  46223  etransclem19  46224  etransclem20  46225  etransclem21  46226  etransclem22  46227  etransclem23  46228  etransclem24  46229  etransclem25  46230  etransclem27  46232  etransclem32  46237  etransclem35  46240  etransclem41  46246  etransclem44  46249  etransclem46  46251  modmknepk  47336  iccpartigtl  47397  iccpartgt  47401  iccpartgel  47403  iccelpart  47407  odz2prm2pw  47537  fmtnoprmfac1  47539  fmtnoprmfac2  47541  2pwp1prm  47563  sfprmdvdsmersenne  47577  lighneallem4a  47582  proththdlem  47587  proththd  47588  perfectALTVlem1  47695  perfectALTVlem2  47696  perfectALTV  47697  fpprwpprb  47714  gpgedgvtx1  48026  logbpw2m1  48529  nnpw2blenfzo  48543  nnolog2flm1  48552  dignn0fr  48563  nn0sumshdiglemA  48581  nn0sumshdiglemB  48582