Theorem nn0zd 12584

Description: A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
nn0zd.1	⊢ (𝜑 → 𝐴 ∈ ℕ0)

Assertion

Ref	Expression
nn0zd	⊢ (𝜑 → 𝐴 ∈ ℤ)

Proof of Theorem nn0zd

Step	Hyp	Ref	Expression
1		nn0ssz 12581	. 2 ⊢ ℕ0 ⊆ ℤ
2		nn0zd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sselid 3981	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2107  ℕ₀cn0 12472  ℤcz 12558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-i2m1 11178  ax-1ne0 11179  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-neg 11447  df-nn 12213  df-n0 12473  df-z 12559

This theorem is referenced by:  nnzd  12585  eluzmn  12829  difelfznle  13615  zmodfz  13858  expnegz  14062  expaddzlem  14071  expaddz  14072  expmulz  14074  faclbnd  14250  bcpasc  14281  hashf1  14418  fz1isolem  14422  hashge2el2dif  14441  hashtpg  14446  wrdffz  14485  ffz0iswrd  14491  wrdsymb0  14499  wrdlenge1n0  14500  ccatcl  14524  ccatval3  14529  ccatsymb  14532  ccatval21sw  14535  ccatass  14538  ccatrn  14539  lswccatn0lsw  14541  ccats1val2  14577  swrdnd  14604  swrdccat2  14619  pfxtrcfv0  14644  pfxtrcfvl  14647  pfxccat1  14652  swrdccatin2  14679  pfxccatin12  14683  pfxccatpfx2  14687  pfxccat3a  14688  splfv2a  14706  splval2  14707  revcl  14711  revccat  14716  revrev  14717  cshwmodn  14745  cshwsublen  14746  cshwn  14747  cshwidxmod  14753  2cshwid  14764  3cshw  14768  cshweqdif2  14769  revco  14785  ccatco  14786  ccat2s1fvwALT  14906  ofccat  14916  zabscl  15260  absrdbnd  15288  iseraltlem3  15630  fsum0diaglem  15722  modfsummods  15739  binomlem  15775  binom1p  15777  incexc2  15784  climcndslem1  15795  geoser  15813  pwm1geoser  15815  geolim2  15817  mertenslem1  15830  mertenslem2  15831  mertens  15832  binomfallfaclem2  15984  binomrisefac  15986  fallfacval4  15987  bpolydiflem  15998  ruclem10  16182  sumodd  16331  divalglem9  16344  divalgmod  16349  bitsfzolem  16375  bitsfzo  16376  bitsmod  16377  bitsfi  16378  bitsinv1lem  16382  sadcaddlem  16398  sadadd3  16402  sadaddlem  16407  sadadd  16408  sadasslem  16411  sadass  16412  sadeq  16413  bitsres  16414  bitsuz  16415  bitsshft  16416  smuval2  16423  smupvallem  16424  smupval  16429  smueqlem  16431  smumullem  16433  smumul  16434  gcdcllem1  16440  zeqzmulgcd  16451  gcd0id  16460  gcdneg  16463  modgcd  16474  gcdmultipled  16476  bezoutlem4  16484  dvdsgcdb  16487  gcdass  16489  mulgcd  16490  gcdzeq  16494  dvdsmulgcd  16497  bezoutr  16505  bezoutr1  16506  nn0seqcvgd  16507  algfx  16517  eucalginv  16521  eucalg  16524  gcddvdslcm  16539  lcmneg  16540  lcmgcdlem  16543  lcmdvds  16545  lcmgcdeq  16549  lcmdvdsb  16550  lcmass  16551  lcmftp  16573  lcmfunsnlem1  16574  lcmfunsnlem2lem1  16575  lcmfunsnlem2lem2  16576  lcmfunsnlem2  16577  lcmfdvdsb  16580  lcmfun  16582  lcmfass  16583  mulgcddvds  16592  rpmulgcd2  16593  qredeu  16595  divgcdcoprm0  16602  sqnprm  16639  divnumden  16684  powm2modprm  16736  coprimeprodsq  16741  iserodd  16768  pclem  16771  pcpre1  16775  pcpremul  16776  pcqcl  16789  pcdvdsb  16802  pcidlem  16805  pc2dvds  16812  pcprmpw2  16815  dvdsprmpweqle  16819  pcadd  16822  pcfac  16832  pcbc  16833  pockthlem  16838  prmreclem2  16850  prmreclem3  16851  mul4sqlem  16886  4sqlem11  16888  4sqlem12  16889  4sqlem14  16891  vdwapun  16907  prmgaplcmlem1  16984  lagsubg  19072  psgnuni  19367  psgnran  19383  odmodnn0  19408  mndodconglem  19409  mndodcong  19410  odm1inv  19421  odmulg2  19423  odmulg  19424  odmulgeq  19425  odbezout  19426  odinv  19429  odf1  19430  gexod  19454  gexdvds3  19458  sylow1lem1  19466  sylow1lem3  19468  pgpfi  19473  pgpssslw  19482  sylow2alem2  19486  sylow2blem3  19490  fislw  19493  sylow3lem4  19498  sylow3lem6  19500  efginvrel2  19595  efgredlemf  19609  efgredlemd  19612  efgredlemc  19613  efgredlem  19615  efgcpbllemb  19623  odadd1  19716  odadd2  19717  gexexlem  19720  gexex  19721  torsubg  19722  lt6abl  19763  gsummulg  19810  ablfacrplem  19935  ablfacrp  19936  ablfacrp2  19937  ablfac1b  19940  ablfac1c  19941  ablfac1eulem  19942  ablfac1eu  19943  pgpfac1lem2  19945  pgpfaclem1  19951  ablfaclem3  19957  srgbinomlem3  20051  srgbinomlem4  20052  chrid  21079  znunit  21119  psgnghm  21133  psrbaglefi  21485  psrbaglefiOLD  21486  chfacfscmulfsupp  22361  chfacfpmmulfsupp  22365  cpmadugsumlemF  22378  dyadss  25111  dyaddisjlem  25112  ply1divex  25654  ply1termlem  25717  plyeq0lem  25724  plyaddlem1  25727  plymullem1  25728  coeeulem  25738  coeidlem  25751  coeeq2  25756  coemulhi  25768  dvply1  25797  dvply2g  25798  plydivex  25810  elqaalem2  25833  aareccl  25839  aannenlem1  25841  aalioulem1  25845  taylplem1  25875  taylplem2  25876  taylpfval  25877  dvtaylp  25882  taylthlem2  25886  dvradcnv  25933  abelthlem7  25950  cxpeq  26265  birthdaylem2  26457  ftalem1  26577  basellem3  26587  isppw2  26619  isnsqf  26639  mule1  26652  ppinncl  26678  musum  26695  chtublem  26714  pclogsum  26718  vmasum  26719  dchrabs  26763  bcmax  26781  bposlem1  26787  bposlem6  26792  lgsval2lem  26810  lgsmod  26826  lgsne0  26838  gausslemma2dlem0h  26866  gausslemma2dlem0i  26867  gausslemma2dlem2  26870  gausslemma2dlem6  26875  gausslemma2d  26877  lgseisenlem1  26878  lgseisenlem2  26879  lgseisenlem3  26880  lgseisenlem4  26881  lgsquadlem1  26883  m1lgs  26891  2lgslem1a  26894  2lgslem3a  26899  2lgslem3b  26900  2lgslem3c  26901  2lgslem3d  26902  2lgslem3d1  26906  2lgsoddprmlem2  26912  2sqlem8  26929  2sqcoprm  26938  2sqmod  26939  chebbnd1lem1  26972  dchrisumlem1  26992  dchrisum0flblem1  27011  selberg2lem  27053  ostth2lem2  27137  ostth2lem3  27138  finsumvtxdg2sstep  28806  finsumvtxdgeven  28809  vtxdgoddnumeven  28810  redwlklem  28928  wlkdlem1  28939  pthdlem1  29023  crctcshwlkn0lem4  29067  wwlksnredwwlkn0  29150  wwlksnextproplem2  29164  clwwlkccatlem  29242  clwlkclwwlkfo  29262  clwwlkwwlksb  29307  clwwlkndivn  29333  eupth2lem3lem3  29483  eupth2lem3lem4  29484  eupth2lem3  29489  eupth2lems  29491  numclwwlk5  29641  numclwwlk6  29643  ex-ind-dvds  29714  nndiffz1  31997  prmdvdsbc  32022  ccatf1  32115  pfxlsw2ccat  32116  wrdt2ind  32117  cycpmfv1  32272  cycpmco2lem2  32286  cycpmco2lem3  32287  cycpmco2lem4  32288  cycpmco2lem5  32289  cycpmco2lem6  32290  cycpmco2  32292  cycpmrn  32302  cyc3genpm  32311  cycpmconjslem2  32314  cyc3conja  32316  archirng  32334  archirngz  32335  archiabllem1a  32337  freshmansdream  32381  elrspunidl  32546  asclmulg  32635  ply1degltel  32666  ply1degltdimlem  32707  madjusmdetlem4  32810  qqhval2lem  32961  oddpwdc  33353  eulerpartlems  33359  eulerpartlemb  33367  sseqfv1  33388  sseqfn  33389  sseqmw  33390  sseqf  33391  sseqfv2  33393  sseqp1  33394  ccatmulgnn0dir  33553  signsplypnf  33561  signsply0  33562  signslema  33573  signstfvn  33580  signstfvp  33582  signstfvc  33585  fsum2dsub  33619  reprinfz1  33634  reprfi2  33635  hashrepr  33637  reprdifc  33639  breprexplema  33642  breprexplemc  33644  circlemeth  33652  circlevma  33654  circlemethhgt  33655  hgt750lema  33669  tgoldbachgtde  33672  lpadlem3  33690  revpfxsfxrev  34106  revwlk  34115  subfacval3  34180  bcprod  34708  bccolsum  34709  fwddifnp1  35137  knoppndvlem6  35393  knoppndvlem7  35394  knoppndvlem10  35397  knoppndvlem14  35401  knoppndvlem15  35402  knoppndvlem16  35403  knoppndvlem17  35404  knoppndvlem19  35406  knoppndvlem21  35408  dfgcd3  36205  poimirlem3  36491  poimirlem4  36492  poimirlem6  36494  poimirlem13  36501  poimirlem14  36502  poimirlem17  36505  poimirlem21  36509  poimirlem22  36510  poimirlem23  36511  poimirlem26  36514  poimirlem27  36515  poimirlem31  36519  geomcau  36627  bccl2d  40857  lcmineqlem12  40905  lcmineqlem17  40910  dvrelogpow2b  40933  aks4d1p1p2  40935  aks4d1p1p4  40936  aks4d1p1p6  40938  aks4d1p1p7  40939  aks4d1p1p5  40940  aks4d1p1  40941  aks4d1p3  40943  aks4d1p6  40946  aks4d1p8d2  40950  aks4d1p8d3  40951  aks4d1p8  40952  aks6d1c2p2  40957  2np3bcnp1  40960  sticksstones5  40966  sticksstones6  40967  sticksstones7  40968  sticksstones10  40971  sticksstones11  40972  sticksstones12a  40973  sticksstones12  40974  sticksstones22  40984  prodsplit  41021  frlmvscadiccat  41080  sumcubes  41211  gcdle1d  41221  gcdle2d  41222  fltdiv  41378  flt4lem4  41391  fltnltalem  41404  eldioph2lem1  41498  pellexlem5  41571  congrep  41712  jm2.18  41727  jm2.19lem1  41728  jm2.19lem2  41729  jm2.19  41732  jm2.22  41734  jm2.23  41735  jm2.20nn  41736  jm2.25  41738  jm2.26a  41739  jm2.26lem3  41740  jm2.26  41741  jm2.27a  41744  jm2.27b  41745  jm2.27c  41746  jm3.1  41759  expdiophlem1  41760  hbtlem5  41870  radcnvrat  43073  nzin  43077  bccbc  43104  binomcxplemnn0  43108  binomcxplemnotnn0  43115  fprodexp  44310  mccllem  44313  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnxpaek  44658  dvnmul  44659  dvnprodlem1  44662  dvnprodlem2  44663  wallispilem1  44781  wallispilem5  44785  stirlinglem3  44792  stirlinglem5  44794  stirlinglem7  44796  stirlinglem8  44797  fourierdlem102  44924  fourierdlem114  44936  sqwvfoura  44944  elaa2lem  44949  etransclem10  44960  etransclem20  44970  etransclem21  44971  etransclem22  44972  etransclem23  44973  etransclem24  44974  etransclem27  44977  etransclem28  44978  etransclem35  44985  etransclem38  44988  etransclem44  44994  etransclem45  44995  etransclem46  44996  sge0ad2en  45147  fsummmodsnunz  46043  fmtnoge3  46198  fmtnof1  46203  fmtnorec1  46205  sqrtpwpw2p  46206  fmtnodvds  46212  goldbachthlem2  46214  fmtnoprmfac2lem1  46234  lighneallem3  46275  lighneallem4b  46277  lighneallem4  46278  ssnn0ssfz  47025  altgsumbcALT  47029  flnn0ohalf  47220  dig2nn1st  47291  0dig2nn0o  47299  aacllem  47848