Theorem nnnn0d 12560

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℕcn 12228  ℕ₀cn0 12499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-ss 3922  df-n0 12500

This theorem is referenced by:  nn0ge2m1nn0  12570  nnzd  12612  eluzge2nn0  12911  expgt1  14132  expaddzlem  14137  expaddz  14138  expmulz  14140  expmulnbnd  14267  exp11nnd  14293  facwordi  14321  faclbnd  14322  facavg  14333  bcm1k  14347  wrdeqs1cat  14753  cshwcsh2id  14861  relexpsucnnr  15058  isercolllem2  15713  bcxmas  15885  climcndslem1  15899  climcndslem2  15900  climcnds  15901  pwdif  15918  geo2sum  15923  mertenslem1  15934  prodmolem3  15983  prodmolem2a  15984  bpolydiflem  16103  eftabs  16124  efcllem  16126  eftlub  16160  eirrlem  16255  rpnnen2lem9  16273  rpnnen2lem11  16275  dvdsfac  16379  pwp1fsum  16444  oddpwp1fsum  16445  bitsfzo  16488  bitsfi  16490  sadcaddlem  16510  smumullem  16545  gcdcl  16559  dvdsgcdidd  16590  mulgcd  16601  rplpwr  16611  rprpwr  16612  rppwr  16613  nn0rppwr  16614  expgcd  16616  lcmcl  16654  lcmgcdnn  16664  lcmfcl  16681  nprmdvds1  16760  rpexp  16776  prmdvdsbc  16780  zsqrtelqelz  16812  phiprmpw  16830  eulerthlem2  16836  eulerth  16837  fermltl  16838  odzcllem  16847  odzdvds  16850  odzphi  16851  prm23lt5  16869  pythagtriplem6  16876  pythagtriplem7  16877  pcprmpw2  16937  dvdsprmpweqle  16941  pcprod  16950  pcfac  16954  pcbc  16955  expnprm  16957  pockthlem  16960  pockthg  16961  prmunb  16969  prmreclem2  16972  prmreclem3  16973  prmreclem4  16974  prmreclem5  16975  prmreclem6  16976  mul4sqlem  17008  4sqlem11  17010  4sqlem17  17016  vdwlem1  17036  vdwlem5  17040  vdwlem6  17041  vdwlem8  17043  vdwlem9  17044  vdwlem11  17046  vdwlem12  17047  vdwnnlem3  17052  ramz2  17079  ramub1lem1  17081  ramub1lem2  17082  ramub1  17083  prmgaplem3  17108  2expltfac  17147  psgnunilem3  19561  odfval  19597  mndodconglem  19606  gexcl3  19652  pgpfi1  19660  sylow1lem1  19663  gexexlem  19917  prmcyg  19959  gsumval3  19972  ablfacrplem  20132  ablfacrp  20133  ablfacrp2  20134  ablfac1eu  20140  prmgrpsimpgd  20181  srgbinomlem3  20305  srgbinomlem4  20306  fermltlchr  21679  freshmansdream  21724  chfacfscmulgsum  23017  chfacfpmmulgsum  23021  cpmadugsumlemF  23033  ovoliunlem1  25661  mbfi1fseqlem1  25874  mbfi1fseqlem3  25876  mbfi1fseqlem5  25878  itg2cnlem2  25921  plyn0mulidp  26442  dvply1  26445  aalioulem2  26496  aalioulem5  26499  aaliou3lem1  26505  aaliou3lem2  26506  aaliou3lem8  26508  aaliou3lem6  26511  taylthlem1  26536  taylthlem2  26537  pserdvlem2  26591  cxpeq  26922  zrtelqelz  26923  dmgmdivn0  27192  lgamgulmlem5  27197  lgamcvg2  27219  wilthlem1  27232  ftalem1  27237  ftalem2  27238  ftalem4  27240  ftalem5  27241  basellem2  27246  basellem3  27247  basellem4  27248  basellem5  27249  isppw2  27279  mpodvdsmulf1o  27358  dvdsmulf1o  27360  sgmmul  27365  fsumvma2  27378  chpchtsum  27383  logfacubnd  27385  mersenne  27391  perfect1  27392  perfectlem1  27393  perfectlem2  27394  perfect  27395  dchrelbas3  27402  dchrelbasd  27403  dchrzrh1  27408  dchrzrhmul  27410  dchrmulcl  27413  dchrn0  27414  dchrfi  27419  dchrghm  27420  dchrabs  27424  dchrinv  27425  dchrptlem1  27428  dchrptlem2  27429  dchrptlem3  27430  dchrpt  27431  dchrsum2  27432  sum2dchr  27438  pcbcctr  27440  bcmono  27441  bclbnd  27444  bposlem1  27448  bposlem3  27450  bposlem5  27452  bposlem6  27453  lgslem1  27461  lgsval2lem  27471  lgsvalmod  27480  lgsmod  27487  lgsdirprm  27495  lgsne0  27499  lgsqrlem1  27510  lgsqrlem2  27511  lgsqrlem3  27512  lgsqrlem4  27513  gausslemma2dlem0b  27521  gausslemma2dlem0c  27522  gausslemma2dlem1  27530  gausslemma2dlem7  27537  gausslemma2d  27538  lgseisenlem1  27539  lgseisenlem2  27540  lgseisenlem3  27541  lgseisenlem4  27542  lgseisen  27543  lgsquadlem2  27545  lgsquadlem3  27546  m1lgs  27552  2lgslem1a  27555  2sqlem3  27584  2sqblem  27595  chebbnd1lem1  27633  chebbnd1lem3  27635  rplogsumlem2  27649  rpvmasumlem  27651  dchrisumlem1  27653  dchrisumlem2  27654  dchrmusum2  27658  dchrvmasumlem3  27663  dchrisum0ff  27671  dchrisum0flblem1  27672  rpvmasum2  27676  dchrisum0re  27677  dchrisum0lem2a  27681  dirith  27693  mudivsum  27694  pntpbnd1a  27749  pntlemq  27765  pntlemr  27766  pntlemj  27767  ostth2lem1  27782  ostth2lem2  27798  ostth2lem3  27799  ostth2  27801  crctcshwlkn0lem6  30164  hashecclwwlkn1  30428  umgrhashecclwwlk  30429  clwwlknon  30441  eucrctshift  30594  numclwlk1lem2  30721  nrt2irr  30824  dipcl  31064  dipcn  31072  bcm1n  33140  expgt0b  33161  nexple  33177  2exple2exp  33178  oexpled  33180  wrdpmtrlast  33413  psgnfzto1st  33425  isarchi2  33505  submarchi  33506  znfermltl  33681  fldextrspundgdvdslem  34070  fldextrspundgdvds  34071  fldext2rspun  34072  constrext2chnlem  34140  cos9thpiminplylem2  34173  submateqlem1  34197  madjusmdetlem2  34218  madjusmdetlem4  34220  mdetlap  34222  oddpwdc  34744  eulerpartlemsv2  34748  eulerpartlemsf  34749  eulerpartlems  34750  eulerpartlemv  34754  eulerpartlemb  34758  signsvtn0  34957  fsum2dsub  34994  reprinfz1  35009  reprpmtf1o  35013  circlemeth  35027  circlemethnat  35028  hgt750lemb  35043  hgt750lema  35044  hgt750leme  35045  tgoldbachgtde  35047  tgoldbachgtda  35048  lpadleft  35073  subfacp1lem1  35671  subfacp1lem6  35677  subfaclim  35680  erdszelem8  35690  erdszelem10  35692  cvmliftlem10  35786  faclim2  36240  poimirlem7  38278  poimirlem17  38288  poimirlem18  38289  poimirlem20  38291  poimirlem21  38292  poimirlem22  38293  poimirlem25  38296  poimirlem26  38297  poimirlem27  38298  poimirlem28  38299  poimirlem32  38303  nninfnub  38402  bfplem1  38473  zndvdchrrhm  42740  lcmineqlem1  42796  lcmineqlem2  42797  lcmineqlem8  42803  lcmineqlem10  42805  lcmineqlem11  42806  lcmineqlem15  42810  lcmineqlem16  42811  lcmineqlem18  42813  lcmineqlem19  42814  lcmineqlem20  42815  lcmineqlem21  42816  lcmineqlem22  42817  3lexlogpow2ineq2  42826  dvrelogpow2b  42835  aks4d1p1p2  42837  aks4d1p1p4  42838  aks4d1p1  42843  aks4d1p3  42845  aks4d1p7d1  42849  aks4d1p7  42850  aks4d1p8  42854  aks4d1p9  42855  isprimroot2  42861  primrootsunit1  42864  primrootscoprmpow  42866  posbezout  42867  primrootscoprbij  42869  primrootlekpowne0  42872  primrootspoweq0  42873  aks6d1c1p2  42876  aks6d1c1p3  42877  aks6d1c1p4  42878  aks6d1c1p5  42879  aks6d1c1p7  42880  aks6d1c1p6  42881  aks6d1c1p8  42882  aks6d1c2p2  42886  hashscontpowcl  42887  hashscontpow1  42888  hashscontpow  42889  aks6d1c4  42891  aks6d1c2lem3  42893  aks6d1c2lem4  42894  aks6d1c2  42897  sticksstones6  42918  sticksstones7  42919  sticksstones10  42922  sticksstones12a  42924  sticksstones12  42925  sticksstones20  42933  sticksstones22  42935  aks6d1c6lem2  42938  aks6d1c6lem3  42939  aks6d1c6lem4  42940  aks6d1c6isolem1  42941  aks6d1c6isolem2  42942  aks6d1c6lem5  42944  bcled  42945  bcle2d  42946  aks6d1c7lem1  42947  aks6d1c7  42951  aks5lem2  42954  aks5lem3a  42956  aks5lem5a  42958  grpods  42961  unitscyglem2  42963  unitscyglem4  42965  aks5lem7  42967  aks5  42971  sumcubes  43074  oexpreposd  43083  exp11d  43087  dvdsexpb  43096  fiabv  43304  fsuppind  43322  dffltz  43366  fltdvdsabdvdsc  43370  fltne  43376  flt4lem4  43381  flt4lem7  43391  fltltc  43393  fltnltalem  43394  fltnlta  43395  3rexfrabdioph  43524  4rexfrabdioph  43525  6rexfrabdioph  43526  7rexfrabdioph  43527  irrapxlem5  43553  pellexlem2  43557  pellexlem6  43561  pell14qrgt0  43586  pell1qrge1  43597  pellfundgt1  43610  ltrmxnn0  43676  jm2.26lem3  43728  jm2.27a  43732  jm2.27c  43734  rmxdiophlem  43742  jm3.1lem1  43744  jm3.1lem2  43745  jm3.1lem3  43746  jm3.1  43747  dgrsub2  43862  mpaaeu  43877  idomsubgmo  43920  relexpxpmin  44443  nzprmdif  45029  binomcxplemwb  45058  fperiodmul  46023  xralrple4  46088  fsumnncl  46288  dvsinexp  46625  dvxpaek  46654  itgsinexplem1  46668  stoweidlem1  46715  stoweidlem17  46731  stoweidlem25  46739  stoweidlem34  46748  stoweidlem38  46752  stoweidlem40  46754  stoweidlem42  46756  stoweidlem45  46759  stirlinglem4  46791  stirlinglem5  46792  stirlinglem10  46797  stirlinglem13  46800  dirkertrigeq  46815  fourierdlem21  46842  fourierdlem25  46846  fourierdlem48  46868  fourierdlem54  46874  fourierdlem64  46884  fourierdlem65  46885  fourierdlem73  46893  fourierdlem81  46901  fourierdlem83  46903  fourierdlem92  46912  fourierdlem103  46923  fourierdlem104  46924  fourierdlem112  46932  fourierdlem113  46933  etransclem1  46949  etransclem4  46952  etransclem8  46956  etransclem15  46963  etransclem17  46965  etransclem18  46966  etransclem19  46967  etransclem20  46968  etransclem21  46969  etransclem22  46970  etransclem23  46971  etransclem24  46972  etransclem25  46973  etransclem27  46975  etransclem32  46980  etransclem35  46983  etransclem41  46989  etransclem44  46992  etransclem46  46994  modmknepk  48105  iccpartigtl  48172  iccpartgt  48176  iccpartgel  48178  iccelpart  48182  odz2prm2pw  48315  fmtnoprmfac1  48317  fmtnoprmfac2  48319  2pwp1prm  48341  sfprmdvdsmersenne  48355  lighneallem4a  48360  proththdlem  48365  proththd  48366  perfectALTVlem1  48486  perfectALTVlem2  48487  perfectALTV  48488  fpprwpprb  48505  gpgedgvtx1  48827  logbpw2m1  49347  nnpw2blenfzo  49361  nnolog2flm1  49370  dignn0fr  49381  nn0sumshdiglemA  49399  nn0sumshdiglemB  49400