Theorem nn0zd 12562

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 12559	. 2 ⊢ ℕ0 ⊆ ℤ
2		nn0zd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sselid 3947	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2109  ℕ₀cn0 12449  ℤcz 12536

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-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-neg 11415  df-nn 12194  df-n0 12450  df-z 12537

This theorem is referenced by:  nnzd  12563  eluzmn  12807  difelfznle  13610  zmodfz  13862  expnegz  14068  expaddzlem  14077  expaddz  14078  expmulz  14080  faclbnd  14262  bcpasc  14293  hashf1  14429  fz1isolem  14433  hashge2el2dif  14452  hashtpg  14457  wrdffz  14507  ffz0iswrd  14513  wrdsymb0  14521  wrdlenge1n0  14522  ccatcl  14546  ccatval3  14551  ccatsymb  14554  ccatval21sw  14557  ccatass  14560  ccatrn  14561  lswccatn0lsw  14563  ccats1val2  14599  swrdnd  14626  swrdccat2  14641  pfxtrcfv0  14666  pfxtrcfvl  14669  pfxccat1  14674  swrdccatin2  14701  pfxccatin12  14705  pfxccatpfx2  14709  pfxccat3a  14710  splfv2a  14728  splval2  14729  revcl  14733  revccat  14738  revrev  14739  cshwmodn  14767  cshwsublen  14768  cshwn  14769  cshwidxmod  14775  2cshwid  14786  3cshw  14790  cshweqdif2  14791  revco  14807  ccatco  14808  ccat2s1fvwALT  14928  ofccat  14942  zabscl  15286  absrdbnd  15315  iseraltlem3  15657  fsum0diaglem  15749  modfsummods  15766  binomlem  15802  binom1p  15804  incexc2  15811  climcndslem1  15822  geoser  15840  pwm1geoser  15842  geolim2  15844  mertenslem1  15857  mertenslem2  15858  mertens  15859  binomfallfaclem2  16013  binomrisefac  16015  fallfacval4  16016  bpolydiflem  16027  ruclem10  16214  sumodd  16365  divalglem9  16378  divalgmod  16383  bitsfzolem  16411  bitsfzo  16412  bitsmod  16413  bitsfi  16414  bitsinv1lem  16418  sadcaddlem  16434  sadadd3  16438  sadaddlem  16443  sadadd  16444  sadasslem  16447  sadass  16448  sadeq  16449  bitsres  16450  bitsuz  16451  bitsshft  16452  smuval2  16459  smupvallem  16460  smupval  16465  smueqlem  16467  smumullem  16469  smumul  16470  gcdcllem1  16476  zeqzmulgcd  16487  gcd0id  16496  gcdneg  16499  modgcd  16509  gcdmultipled  16511  bezoutlem4  16519  dvdsgcdb  16522  gcdass  16524  mulgcd  16525  gcdzeq  16529  dvdsmulgcd  16533  bezoutr  16545  bezoutr1  16546  nn0seqcvgd  16547  algfx  16557  eucalginv  16561  eucalg  16564  gcddvdslcm  16579  lcmneg  16580  lcmgcdlem  16583  lcmdvds  16585  lcmgcdeq  16589  lcmdvdsb  16590  lcmass  16591  lcmftp  16613  lcmfunsnlem1  16614  lcmfunsnlem2lem1  16615  lcmfunsnlem2lem2  16616  lcmfunsnlem2  16617  lcmfdvdsb  16620  lcmfun  16622  lcmfass  16623  mulgcddvds  16632  rpmulgcd2  16633  qredeu  16635  divgcdcoprm0  16642  sqnprm  16679  prmdvdsbc  16703  divnumden  16725  powm2modprm  16781  coprimeprodsq  16786  iserodd  16813  pclem  16816  pcpre1  16820  pcpremul  16821  pcqcl  16834  pcdvdsb  16847  pcidlem  16850  pc2dvds  16857  pcprmpw2  16860  dvdsprmpweqle  16864  pcadd  16867  pcfac  16877  pcbc  16878  pockthlem  16883  prmreclem2  16895  prmreclem3  16896  mul4sqlem  16931  4sqlem11  16933  4sqlem12  16934  4sqlem14  16936  vdwapun  16952  prmgaplcmlem1  17029  lagsubg  19134  psgnuni  19436  psgnran  19452  odmodnn0  19477  mndodconglem  19478  mndodcong  19479  odm1inv  19490  odmulg2  19492  odmulg  19493  odmulgeq  19494  odbezout  19495  odinv  19498  odf1  19499  gexod  19523  gexdvds3  19527  sylow1lem1  19535  sylow1lem3  19537  pgpfi  19542  pgpssslw  19551  sylow2alem2  19555  sylow2blem3  19559  fislw  19562  sylow3lem4  19567  sylow3lem6  19569  efginvrel2  19664  efgredlemf  19678  efgredlemd  19681  efgredlemc  19682  efgredlem  19684  efgcpbllemb  19692  odadd1  19785  odadd2  19786  gexexlem  19789  gexex  19790  torsubg  19791  lt6abl  19832  gsummulg  19879  ablfacrplem  20004  ablfacrp  20005  ablfacrp2  20006  ablfac1b  20009  ablfac1c  20010  ablfac1eulem  20011  ablfac1eu  20012  pgpfac1lem2  20014  pgpfaclem1  20020  ablfaclem3  20026  srgbinomlem3  20144  srgbinomlem4  20145  chrid  21442  znunit  21480  freshmansdream  21491  psgnghm  21496  asclmulg  21818  psrbaglefi  21842  psdvsca  22058  psdmul  22060  chfacfscmulfsupp  22753  chfacfpmmulfsupp  22757  cpmadugsumlemF  22770  dyadss  25502  dyaddisjlem  25503  ply1divex  26049  ply1termlem  26115  plyeq0lem  26122  plyaddlem1  26125  plymullem1  26126  coeeulem  26136  coeidlem  26149  coeeq2  26154  coemulhi  26166  dvply1  26198  dvply2g  26199  dvply2gOLD  26200  plydivex  26212  elqaalem2  26235  aareccl  26241  aannenlem1  26243  aalioulem1  26247  taylplem1  26277  taylplem2  26278  taylpfval  26279  dvtaylp  26285  taylthlem2  26289  taylthlem2OLD  26290  dvradcnv  26337  abelthlem7  26355  cxpeq  26674  birthdaylem2  26869  ftalem1  26990  basellem3  27000  isppw2  27032  isnsqf  27052  mule1  27065  ppinncl  27091  musum  27108  chtublem  27129  pclogsum  27133  vmasum  27134  dchrabs  27178  bcmax  27196  bposlem1  27202  bposlem6  27207  lgsval2lem  27225  lgsmod  27241  lgsne0  27253  gausslemma2dlem0h  27281  gausslemma2dlem0i  27282  gausslemma2dlem2  27285  gausslemma2dlem6  27290  gausslemma2d  27292  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem3  27295  lgseisenlem4  27296  lgsquadlem1  27298  m1lgs  27306  2lgslem1a  27309  2lgslem3a  27314  2lgslem3b  27315  2lgslem3c  27316  2lgslem3d  27317  2lgslem3d1  27321  2lgsoddprmlem2  27327  2sqlem8  27344  2sqcoprm  27353  2sqmod  27354  chebbnd1lem1  27387  dchrisumlem1  27407  dchrisum0flblem1  27426  selberg2lem  27468  ostth2lem2  27552  ostth2lem3  27553  finsumvtxdg2sstep  29484  finsumvtxdgeven  29487  vtxdgoddnumeven  29488  redwlklem  29606  wlkdlem1  29617  pthdlem1  29703  crctcshwlkn0lem4  29750  wwlksnredwwlkn0  29833  wwlksnextproplem2  29847  clwwlkccatlem  29925  clwlkclwwlkfo  29945  clwwlkwwlksb  29990  clwwlkndivn  30016  eupth2lem3lem3  30166  eupth2lem3lem4  30167  eupth2lem3  30172  eupth2lems  30174  numclwwlk5  30324  numclwwlk6  30326  ex-ind-dvds  30397  nndiffz1  32716  elfzodif0  32724  fzo0opth  32735  ccatf1  32877  ccatdmss  32878  pfxlsw2ccat  32879  wrdt2ind  32882  chnind  32944  chnub  32945  gsumwrd2dccatlem  33013  cycpmfv1  33077  cycpmco2lem2  33091  cycpmco2lem3  33092  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2  33097  cycpmrn  33107  cyc3genpm  33116  cycpmconjslem2  33119  cyc3conja  33121  archirng  33149  archirngz  33150  archiabllem1a  33152  elrspunidl  33406  ply1degltel  33567  ply1degltdimlem  33625  fldextrspundgdvds  33683  algextdeglem8  33721  rtelextdg2  33724  constrext2chnlem  33747  cos9thpiminplylem2  33780  cos9thpiminplylem3  33781  cos9thpiminplylem6  33784  cos9thpiminply  33785  madjusmdetlem4  33827  zrhcntr  33976  qqhval2lem  33978  oddpwdc  34352  eulerpartlems  34358  eulerpartlemb  34366  sseqfv1  34387  sseqfn  34388  sseqmw  34389  sseqf  34390  sseqfv2  34392  sseqp1  34393  ccatmulgnn0dir  34540  signsplypnf  34548  signsply0  34549  signslema  34560  signstfvn  34567  signstfvp  34569  signstfvc  34572  fsum2dsub  34605  reprinfz1  34620  reprfi2  34621  hashrepr  34623  reprdifc  34625  breprexplema  34628  breprexplemc  34630  circlemeth  34638  circlevma  34640  circlemethhgt  34641  hgt750lema  34655  tgoldbachgtde  34658  lpadlem3  34676  revpfxsfxrev  35110  revwlk  35119  subfacval3  35183  bcprod  35732  bccolsum  35733  fwddifnp1  36160  knoppndvlem6  36512  knoppndvlem7  36513  knoppndvlem10  36516  knoppndvlem14  36520  knoppndvlem15  36521  knoppndvlem16  36522  knoppndvlem17  36523  knoppndvlem19  36525  knoppndvlem21  36527  dfgcd3  37319  poimirlem3  37624  poimirlem4  37625  poimirlem6  37627  poimirlem13  37634  poimirlem14  37635  poimirlem17  37638  poimirlem21  37642  poimirlem22  37643  poimirlem23  37644  poimirlem26  37647  poimirlem27  37648  poimirlem31  37652  geomcau  37760  bccl2d  41986  lcmineqlem12  42035  lcmineqlem17  42040  dvrelogpow2b  42063  aks4d1p1p2  42065  aks4d1p1p4  42066  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p1  42071  aks4d1p3  42073  aks4d1p6  42076  aks4d1p8d2  42080  aks4d1p8d3  42081  aks4d1p8  42082  primrootscoprmpow  42094  primrootlekpowne0  42100  aks6d1c1  42111  aks6d1c2p2  42114  aks6d1c2lem4  42122  aks6d1c2  42125  aks6d1c5lem3  42132  aks6d1c5lem2  42133  2np3bcnp1  42139  sticksstones5  42145  sticksstones6  42146  sticksstones7  42147  sticksstones10  42150  sticksstones11  42151  sticksstones12a  42152  sticksstones12  42153  sticksstones22  42163  aks6d1c6lem3  42167  bcled  42173  bcle2d  42174  aks6d1c7lem1  42175  aks6d1c7lem2  42176  grpods  42189  unitscyglem2  42191  unitscyglem4  42193  aks5lem8  42196  sumcubes  42308  gcdle1d  42325  gcdle2d  42326  frlmvscadiccat  42501  fltdiv  42631  flt4lem4  42644  fltnltalem  42657  eldioph2lem1  42755  pellexlem5  42828  congrep  42969  jm2.18  42984  jm2.19lem1  42985  jm2.19lem2  42986  jm2.19  42989  jm2.22  42991  jm2.23  42992  jm2.20nn  42993  jm2.25  42995  jm2.26a  42996  jm2.26lem3  42997  jm2.26  42998  jm2.27a  43001  jm2.27b  43002  jm2.27c  43003  jm3.1  43016  expdiophlem1  43017  hbtlem5  43124  radcnvrat  44310  nzin  44314  bccbc  44341  binomcxplemnn0  44345  binomcxplemnotnn0  44352  fprodexp  45599  mccllem  45602  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnxpaek  45947  dvnmul  45948  dvnprodlem1  45951  dvnprodlem2  45952  wallispilem1  46070  wallispilem5  46074  stirlinglem3  46081  stirlinglem5  46083  stirlinglem7  46085  stirlinglem8  46086  fourierdlem102  46213  fourierdlem114  46225  sqwvfoura  46233  elaa2lem  46238  etransclem10  46249  etransclem20  46259  etransclem21  46260  etransclem22  46261  etransclem23  46262  etransclem24  46263  etransclem27  46266  etransclem28  46267  etransclem35  46274  etransclem38  46277  etransclem44  46283  etransclem45  46284  etransclem46  46285  sge0ad2en  46436  fsummmodsnunz  47380  fmtnoge3  47535  fmtnof1  47540  fmtnorec1  47542  sqrtpwpw2p  47543  fmtnodvds  47549  goldbachthlem2  47551  fmtnoprmfac2lem1  47571  lighneallem3  47612  lighneallem4b  47614  lighneallem4  47615  ssnn0ssfz  48341  altgsumbcALT  48345  flnn0ohalf  48527  dig2nn1st  48598  0dig2nn0o  48606  aacllem  49794