Theorem nn0zd 12636

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℕ₀cn0 12523  ℤcz 12610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-neg 11492  df-nn 12264  df-n0 12524  df-z 12611

This theorem is referenced by:  nnzd  12637  eluzmn  12882  difelfznle  13678  zmodfz  13929  expnegz  14133  expaddzlem  14142  expaddz  14143  expmulz  14145  faclbnd  14325  bcpasc  14356  hashf1  14492  fz1isolem  14496  hashge2el2dif  14515  hashtpg  14520  wrdffz  14569  ffz0iswrd  14575  wrdsymb0  14583  wrdlenge1n0  14584  ccatcl  14608  ccatval3  14613  ccatsymb  14616  ccatval21sw  14619  ccatass  14622  ccatrn  14623  lswccatn0lsw  14625  ccats1val2  14661  swrdnd  14688  swrdccat2  14703  pfxtrcfv0  14728  pfxtrcfvl  14731  pfxccat1  14736  swrdccatin2  14763  pfxccatin12  14767  pfxccatpfx2  14771  pfxccat3a  14772  splfv2a  14790  splval2  14791  revcl  14795  revccat  14800  revrev  14801  cshwmodn  14829  cshwsublen  14830  cshwn  14831  cshwidxmod  14837  2cshwid  14848  3cshw  14852  cshweqdif2  14853  revco  14869  ccatco  14870  ccat2s1fvwALT  14990  ofccat  15004  zabscl  15348  absrdbnd  15376  iseraltlem3  15716  fsum0diaglem  15808  modfsummods  15825  binomlem  15861  binom1p  15863  incexc2  15870  climcndslem1  15881  geoser  15899  pwm1geoser  15901  geolim2  15903  mertenslem1  15916  mertenslem2  15917  mertens  15918  binomfallfaclem2  16072  binomrisefac  16074  fallfacval4  16075  bpolydiflem  16086  ruclem10  16271  sumodd  16421  divalglem9  16434  divalgmod  16439  bitsfzolem  16467  bitsfzo  16468  bitsmod  16469  bitsfi  16470  bitsinv1lem  16474  sadcaddlem  16490  sadadd3  16494  sadaddlem  16499  sadadd  16500  sadasslem  16503  sadass  16504  sadeq  16505  bitsres  16506  bitsuz  16507  bitsshft  16508  smuval2  16515  smupvallem  16516  smupval  16521  smueqlem  16523  smumullem  16525  smumul  16526  gcdcllem1  16532  zeqzmulgcd  16543  gcd0id  16552  gcdneg  16555  modgcd  16565  gcdmultipled  16567  bezoutlem4  16575  dvdsgcdb  16578  gcdass  16580  mulgcd  16581  gcdzeq  16585  dvdsmulgcd  16589  bezoutr  16601  bezoutr1  16602  nn0seqcvgd  16603  algfx  16613  eucalginv  16617  eucalg  16620  gcddvdslcm  16635  lcmneg  16636  lcmgcdlem  16639  lcmdvds  16641  lcmgcdeq  16645  lcmdvdsb  16646  lcmass  16647  lcmftp  16669  lcmfunsnlem1  16670  lcmfunsnlem2lem1  16671  lcmfunsnlem2lem2  16672  lcmfunsnlem2  16673  lcmfdvdsb  16676  lcmfun  16678  lcmfass  16679  mulgcddvds  16688  rpmulgcd2  16689  qredeu  16691  divgcdcoprm0  16698  sqnprm  16735  prmdvdsbc  16759  divnumden  16781  powm2modprm  16836  coprimeprodsq  16841  iserodd  16868  pclem  16871  pcpre1  16875  pcpremul  16876  pcqcl  16889  pcdvdsb  16902  pcidlem  16905  pc2dvds  16912  pcprmpw2  16915  dvdsprmpweqle  16919  pcadd  16922  pcfac  16932  pcbc  16933  pockthlem  16938  prmreclem2  16950  prmreclem3  16951  mul4sqlem  16986  4sqlem11  16988  4sqlem12  16989  4sqlem14  16991  vdwapun  17007  prmgaplcmlem1  17084  lagsubg  19225  psgnuni  19531  psgnran  19547  odmodnn0  19572  mndodconglem  19573  mndodcong  19574  odm1inv  19585  odmulg2  19587  odmulg  19588  odmulgeq  19589  odbezout  19590  odinv  19593  odf1  19594  gexod  19618  gexdvds3  19622  sylow1lem1  19630  sylow1lem3  19632  pgpfi  19637  pgpssslw  19646  sylow2alem2  19650  sylow2blem3  19654  fislw  19657  sylow3lem4  19662  sylow3lem6  19664  efginvrel2  19759  efgredlemf  19773  efgredlemd  19776  efgredlemc  19777  efgredlem  19779  efgcpbllemb  19787  odadd1  19880  odadd2  19881  gexexlem  19884  gexex  19885  torsubg  19886  lt6abl  19927  gsummulg  19974  ablfacrplem  20099  ablfacrp  20100  ablfacrp2  20101  ablfac1b  20104  ablfac1c  20105  ablfac1eulem  20106  ablfac1eu  20107  pgpfac1lem2  20109  pgpfaclem1  20115  ablfaclem3  20121  srgbinomlem3  20245  srgbinomlem4  20246  chrid  21557  znunit  21599  freshmansdream  21610  psgnghm  21615  asclmulg  21939  psrbaglefi  21963  psdvsca  22185  psdmul  22187  chfacfscmulfsupp  22880  chfacfpmmulfsupp  22884  cpmadugsumlemF  22897  dyadss  25642  dyaddisjlem  25643  ply1divex  26190  ply1termlem  26256  plyeq0lem  26263  plyaddlem1  26266  plymullem1  26267  coeeulem  26277  coeidlem  26290  coeeq2  26295  coemulhi  26307  dvply1  26339  dvply2g  26340  dvply2gOLD  26341  plydivex  26353  elqaalem2  26376  aareccl  26382  aannenlem1  26384  aalioulem1  26388  taylplem1  26418  taylplem2  26419  taylpfval  26420  dvtaylp  26426  taylthlem2  26430  taylthlem2OLD  26431  dvradcnv  26478  abelthlem7  26496  cxpeq  26814  birthdaylem2  27009  ftalem1  27130  basellem3  27140  isppw2  27172  isnsqf  27192  mule1  27205  ppinncl  27231  musum  27248  chtublem  27269  pclogsum  27273  vmasum  27274  dchrabs  27318  bcmax  27336  bposlem1  27342  bposlem6  27347  lgsval2lem  27365  lgsmod  27381  lgsne0  27393  gausslemma2dlem0h  27421  gausslemma2dlem0i  27422  gausslemma2dlem2  27425  gausslemma2dlem6  27430  gausslemma2d  27432  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem3  27435  lgseisenlem4  27436  lgsquadlem1  27438  m1lgs  27446  2lgslem1a  27449  2lgslem3a  27454  2lgslem3b  27455  2lgslem3c  27456  2lgslem3d  27457  2lgslem3d1  27461  2lgsoddprmlem2  27467  2sqlem8  27484  2sqcoprm  27493  2sqmod  27494  chebbnd1lem1  27527  dchrisumlem1  27547  dchrisum0flblem1  27566  selberg2lem  27608  ostth2lem2  27692  ostth2lem3  27693  finsumvtxdg2sstep  29581  finsumvtxdgeven  29584  vtxdgoddnumeven  29585  redwlklem  29703  wlkdlem1  29714  pthdlem1  29798  crctcshwlkn0lem4  29842  wwlksnredwwlkn0  29925  wwlksnextproplem2  29939  clwwlkccatlem  30017  clwlkclwwlkfo  30037  clwwlkwwlksb  30082  clwwlkndivn  30108  eupth2lem3lem3  30258  eupth2lem3lem4  30259  eupth2lem3  30264  eupth2lems  30266  numclwwlk5  30416  numclwwlk6  30418  ex-ind-dvds  30489  nndiffz1  32794  fzo0opth  32812  ccatf1  32917  ccatdmss  32918  pfxlsw2ccat  32919  wrdt2ind  32922  chnind  32984  chnub  32985  gsumwrd2dccatlem  33051  cycpmfv1  33115  cycpmco2lem2  33129  cycpmco2lem3  33130  cycpmco2lem4  33131  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2  33135  cycpmrn  33145  cyc3genpm  33154  cycpmconjslem2  33157  cyc3conja  33159  archirng  33177  archirngz  33178  archiabllem1a  33180  elrspunidl  33435  ply1degltel  33594  ply1degltdimlem  33649  algextdeglem8  33729  rtelextdg2  33732  madjusmdetlem4  33790  zrhcntr  33941  qqhval2lem  33943  oddpwdc  34335  eulerpartlems  34341  eulerpartlemb  34349  sseqfv1  34370  sseqfn  34371  sseqmw  34372  sseqf  34373  sseqfv2  34375  sseqp1  34376  ccatmulgnn0dir  34535  signsplypnf  34543  signsply0  34544  signslema  34555  signstfvn  34562  signstfvp  34564  signstfvc  34567  fsum2dsub  34600  reprinfz1  34615  reprfi2  34616  hashrepr  34618  reprdifc  34620  breprexplema  34623  breprexplemc  34625  circlemeth  34633  circlevma  34635  circlemethhgt  34636  hgt750lema  34650  tgoldbachgtde  34653  lpadlem3  34671  revpfxsfxrev  35099  revwlk  35108  subfacval3  35173  bcprod  35717  bccolsum  35718  fwddifnp1  36146  knoppndvlem6  36499  knoppndvlem7  36500  knoppndvlem10  36503  knoppndvlem14  36507  knoppndvlem15  36508  knoppndvlem16  36509  knoppndvlem17  36510  knoppndvlem19  36512  knoppndvlem21  36514  dfgcd3  37306  poimirlem3  37609  poimirlem4  37610  poimirlem6  37612  poimirlem13  37619  poimirlem14  37620  poimirlem17  37623  poimirlem21  37627  poimirlem22  37628  poimirlem23  37629  poimirlem26  37632  poimirlem27  37633  poimirlem31  37637  geomcau  37745  bccl2d  41972  lcmineqlem12  42021  lcmineqlem17  42026  dvrelogpow2b  42049  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  aks4d1p3  42059  aks4d1p6  42062  aks4d1p8d2  42066  aks4d1p8d3  42067  aks4d1p8  42068  primrootscoprmpow  42080  primrootlekpowne0  42086  aks6d1c1  42097  aks6d1c2p2  42100  aks6d1c2lem4  42108  aks6d1c2  42111  aks6d1c5lem3  42118  aks6d1c5lem2  42119  2np3bcnp1  42125  sticksstones5  42131  sticksstones6  42132  sticksstones7  42133  sticksstones10  42136  sticksstones11  42137  sticksstones12a  42138  sticksstones12  42139  sticksstones22  42149  aks6d1c6lem3  42153  bcled  42159  bcle2d  42160  aks6d1c7lem1  42161  aks6d1c7lem2  42162  grpods  42175  unitscyglem2  42177  unitscyglem4  42179  aks5lem8  42182  prodsplit  42221  sumcubes  42325  gcdle1d  42343  gcdle2d  42344  frlmvscadiccat  42492  fltdiv  42622  flt4lem4  42635  fltnltalem  42648  eldioph2lem1  42747  pellexlem5  42820  congrep  42961  jm2.18  42976  jm2.19lem1  42977  jm2.19lem2  42978  jm2.19  42981  jm2.22  42983  jm2.23  42984  jm2.20nn  42985  jm2.25  42987  jm2.26a  42988  jm2.26lem3  42989  jm2.26  42990  jm2.27a  42993  jm2.27b  42994  jm2.27c  42995  jm3.1  43008  expdiophlem1  43009  hbtlem5  43116  radcnvrat  44309  nzin  44313  bccbc  44340  binomcxplemnn0  44344  binomcxplemnotnn0  44351  fprodexp  45549  mccllem  45552  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnxpaek  45897  dvnmul  45898  dvnprodlem1  45901  dvnprodlem2  45902  wallispilem1  46020  wallispilem5  46024  stirlinglem3  46031  stirlinglem5  46033  stirlinglem7  46035  stirlinglem8  46036  fourierdlem102  46163  fourierdlem114  46175  sqwvfoura  46183  elaa2lem  46188  etransclem10  46199  etransclem20  46209  etransclem21  46210  etransclem22  46211  etransclem23  46212  etransclem24  46213  etransclem27  46216  etransclem28  46217  etransclem35  46224  etransclem38  46227  etransclem44  46233  etransclem45  46234  etransclem46  46235  sge0ad2en  46386  fsummmodsnunz  47299  fmtnoge3  47454  fmtnof1  47459  fmtnorec1  47461  sqrtpwpw2p  47462  fmtnodvds  47468  goldbachthlem2  47470  fmtnoprmfac2lem1  47490  lighneallem3  47531  lighneallem4b  47533  lighneallem4  47534  ssnn0ssfz  48193  altgsumbcALT  48197  flnn0ohalf  48383  dig2nn1st  48454  0dig2nn0o  48462  aacllem  49031