Theorem nn0zd 12540

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕ₀cn0 12428  ℤcz 12515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-i2m1 11097  ax-1ne0 11098  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-neg 11371  df-nn 12166  df-n0 12429  df-z 12516

This theorem is referenced by:  nnzd  12541  eluzmn  12786  difelfznle  13587  elfzodif0  13716  zmodfz  13843  expnegz  14049  expaddzlem  14058  expaddz  14059  expmulz  14061  faclbnd  14243  bcpasc  14274  hashf1  14410  fz1isolem  14414  hashge2el2dif  14433  hashtpg  14438  wrdffz  14488  ffz0iswrd  14494  wrdsymb0  14502  wrdlenge1n0  14503  ccatcl  14527  ccatval3  14532  ccatdmss  14535  ccatsymb  14536  ccatval21sw  14539  ccatass  14542  ccatrn  14543  lswccatn0lsw  14545  ccats1val2  14581  swrdnd  14608  swrdccat2  14623  pfxtrcfv0  14647  pfxtrcfvl  14650  pfxccat1  14655  swrdccatin2  14682  pfxccatin12  14686  pfxccatpfx2  14690  pfxccat3a  14691  splfv2a  14709  splval2  14710  revcl  14714  revccat  14719  revrev  14720  cshwmodn  14748  cshwsublen  14749  cshwn  14750  cshwidxmod  14756  2cshwid  14767  3cshw  14771  cshweqdif2  14772  revco  14787  ccatco  14788  ccat2s1fvwALT  14908  ofccat  14922  zabscl  15266  absrdbnd  15295  iseraltlem3  15637  fsum0diaglem  15729  modfsummods  15747  binomlem  15785  binom1p  15787  incexc2  15794  climcndslem1  15805  geoser  15823  pwm1geoser  15825  geolim2  15827  mertenslem1  15840  mertenslem2  15841  mertens  15842  binomfallfaclem2  15996  binomrisefac  15998  fallfacval4  15999  bpolydiflem  16010  ruclem10  16197  sumodd  16348  divalglem9  16361  divalgmod  16366  bitsfzolem  16394  bitsfzo  16395  bitsmod  16396  bitsfi  16397  bitsinv1lem  16401  sadcaddlem  16417  sadadd3  16421  sadaddlem  16426  sadadd  16427  sadasslem  16430  sadass  16431  sadeq  16432  bitsres  16433  bitsuz  16434  bitsshft  16435  smuval2  16442  smupvallem  16443  smupval  16448  smueqlem  16450  smumullem  16452  smumul  16453  gcdcllem1  16459  zeqzmulgcd  16470  gcd0id  16479  gcdneg  16482  modgcd  16492  gcdmultipled  16494  bezoutlem4  16502  dvdsgcdb  16505  gcdass  16507  mulgcd  16508  gcdzeq  16512  dvdsmulgcd  16516  bezoutr  16528  bezoutr1  16529  nn0seqcvgd  16530  algfx  16540  eucalginv  16544  eucalg  16547  gcddvdslcm  16562  lcmneg  16563  lcmgcdlem  16566  lcmdvds  16568  lcmgcdeq  16572  lcmdvdsb  16573  lcmass  16574  lcmftp  16596  lcmfunsnlem1  16597  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  lcmfunsnlem2  16600  lcmfdvdsb  16603  lcmfun  16605  lcmfass  16606  mulgcddvds  16615  rpmulgcd2  16616  qredeu  16618  divgcdcoprm0  16625  sqnprm  16663  prmdvdsbc  16687  divnumden  16709  powm2modprm  16765  coprimeprodsq  16770  iserodd  16797  pclem  16800  pcpre1  16804  pcpremul  16805  pcqcl  16818  pcdvdsb  16831  pcidlem  16834  pc2dvds  16841  pcprmpw2  16844  dvdsprmpweqle  16848  pcadd  16851  pcfac  16861  pcbc  16862  pockthlem  16867  prmreclem2  16879  prmreclem3  16880  mul4sqlem  16915  4sqlem11  16917  4sqlem12  16918  4sqlem14  16920  vdwapun  16936  prmgaplcmlem1  17013  chnind  18578  chnub  18579  chnpolfz  18590  lagsubg  19161  psgnuni  19465  psgnran  19481  odmodnn0  19506  mndodconglem  19507  mndodcong  19508  odm1inv  19519  odmulg2  19521  odmulg  19522  odmulgeq  19523  odbezout  19524  odinv  19527  odf1  19528  gexod  19552  gexdvds3  19556  sylow1lem1  19564  sylow1lem3  19566  pgpfi  19571  pgpssslw  19580  sylow2alem2  19584  sylow2blem3  19588  fislw  19591  sylow3lem4  19596  sylow3lem6  19598  efginvrel2  19693  efgredlemf  19707  efgredlemd  19710  efgredlemc  19711  efgredlem  19713  efgcpbllemb  19721  odadd1  19814  odadd2  19815  gexexlem  19818  gexex  19819  torsubg  19820  lt6abl  19861  gsummulg  19908  ablfacrplem  20033  ablfacrp  20034  ablfacrp2  20035  ablfac1b  20038  ablfac1c  20039  ablfac1eulem  20040  ablfac1eu  20041  pgpfac1lem2  20043  pgpfaclem1  20049  ablfaclem3  20055  srgbinomlem3  20200  srgbinomlem4  20201  chrid  21515  znunit  21553  freshmansdream  21564  psgnghm  21570  asclmulg  21892  psrbaglefi  21916  psdvsca  22140  psdmul  22142  chfacfscmulfsupp  22834  chfacfpmmulfsupp  22838  cpmadugsumlemF  22851  dyadss  25571  dyaddisjlem  25572  ply1divex  26112  ply1termlem  26178  plyeq0lem  26185  plyaddlem1  26188  plymullem1  26189  coeeulem  26199  coeidlem  26212  coeeq2  26217  coemulhi  26229  dvply1  26260  dvply2g  26261  dvply2gOLD  26262  plydivex  26274  elqaalem2  26297  aareccl  26303  aannenlem1  26305  aalioulem1  26309  taylplem1  26339  taylplem2  26340  taylpfval  26341  dvtaylp  26347  taylthlem2  26351  taylthlem2OLD  26352  dvradcnv  26399  abelthlem7  26416  cxpeq  26734  birthdaylem2  26929  ftalem1  27050  basellem3  27060  isppw2  27092  isnsqf  27112  mule1  27125  ppinncl  27151  musum  27168  chtublem  27188  pclogsum  27192  vmasum  27193  dchrabs  27237  bcmax  27255  bposlem1  27261  bposlem6  27266  lgsval2lem  27284  lgsmod  27300  lgsne0  27312  gausslemma2dlem0h  27340  gausslemma2dlem0i  27341  gausslemma2dlem2  27344  gausslemma2dlem6  27349  gausslemma2d  27351  lgseisenlem1  27352  lgseisenlem2  27353  lgseisenlem3  27354  lgseisenlem4  27355  lgsquadlem1  27357  m1lgs  27365  2lgslem1a  27368  2lgslem3a  27373  2lgslem3b  27374  2lgslem3c  27375  2lgslem3d  27376  2lgslem3d1  27380  2lgsoddprmlem2  27386  2sqlem8  27403  2sqcoprm  27412  2sqmod  27413  chebbnd1lem1  27446  dchrisumlem1  27466  dchrisum0flblem1  27485  selberg2lem  27527  ostth2lem2  27611  ostth2lem3  27612  finsumvtxdg2sstep  29633  finsumvtxdgeven  29636  vtxdgoddnumeven  29637  redwlklem  29753  wlkdlem1  29764  pthdlem1  29849  crctcshwlkn0lem4  29896  wwlksnredwwlkn0  29979  wwlksnextproplem2  29993  clwwlkccatlem  30074  clwlkclwwlkfo  30094  clwwlkwwlksb  30139  clwwlkndivn  30165  eupth2lem3lem3  30315  eupth2lem3lem4  30316  eupth2lem3  30321  eupth2lems  30323  numclwwlk5  30473  numclwwlk6  30475  ex-ind-dvds  30546  nndiffz1  32874  fzo0opth  32891  ccatf1  33024  pfxlsw2ccat  33025  wrdt2ind  33028  gsummulsubdishift1  33144  gsumwrd2dccatlem  33153  cycpmfv1  33189  cycpmco2lem2  33203  cycpmco2lem3  33204  cycpmco2lem4  33205  cycpmco2lem5  33206  cycpmco2lem6  33207  cycpmco2  33209  cycpmrn  33219  cyc3genpm  33228  cycpmconjslem2  33231  cyc3conja  33233  archirng  33264  archirngz  33265  archiabllem1a  33267  gsumind  33420  elrspunidl  33503  ply1coedeg  33664  ply1degltel  33669  gsummoncoe1fz  33673  esplyfval2  33724  esplympl  33726  esplyfval3  33731  esplyindfv  33735  vietalem  33738  ply1degltdimlem  33782  fldextrspundgdvds  33841  algextdeglem8  33884  rtelextdg2  33887  constrext2chnlem  33910  cos9thpiminplylem2  33943  cos9thpiminplylem3  33944  cos9thpiminplylem6  33947  cos9thpiminply  33948  madjusmdetlem4  33990  zrhcntr  34139  qqhval2lem  34141  oddpwdc  34514  eulerpartlems  34520  eulerpartlemb  34528  sseqfv1  34549  sseqfn  34550  sseqmw  34551  sseqf  34552  sseqfv2  34554  sseqp1  34555  ccatmulgnn0dir  34702  signsplypnf  34710  signsply0  34711  signslema  34722  signstfvn  34729  signstfvp  34731  signstfvc  34734  fsum2dsub  34767  reprinfz1  34782  reprfi2  34783  hashrepr  34785  reprdifc  34787  breprexplema  34790  breprexplemc  34792  circlemeth  34800  circlevma  34802  circlemethhgt  34803  hgt750lema  34817  tgoldbachgtde  34820  lpadlem3  34838  revpfxsfxrev  35314  revwlk  35323  subfacval3  35387  bcprod  35936  bccolsum  35937  fwddifnp1  36363  knoppndvlem6  36793  knoppndvlem7  36794  knoppndvlem10  36797  knoppndvlem14  36801  knoppndvlem15  36802  knoppndvlem16  36803  knoppndvlem17  36804  knoppndvlem19  36806  knoppndvlem21  36808  dfgcd3  37654  poimirlem3  37958  poimirlem4  37959  poimirlem6  37961  poimirlem13  37968  poimirlem14  37969  poimirlem17  37972  poimirlem21  37976  poimirlem22  37977  poimirlem23  37978  poimirlem26  37981  poimirlem27  37982  poimirlem31  37986  geomcau  38094  bccl2d  42444  lcmineqlem12  42493  lcmineqlem17  42498  dvrelogpow2b  42521  aks4d1p1p2  42523  aks4d1p1p4  42524  aks4d1p1p6  42526  aks4d1p1p7  42527  aks4d1p1p5  42528  aks4d1p1  42529  aks4d1p3  42531  aks4d1p6  42534  aks4d1p8d2  42538  aks4d1p8d3  42539  aks4d1p8  42540  primrootscoprmpow  42552  primrootlekpowne0  42558  aks6d1c1  42569  aks6d1c2p2  42572  aks6d1c2lem4  42580  aks6d1c2  42583  aks6d1c5lem3  42590  aks6d1c5lem2  42591  2np3bcnp1  42597  sticksstones5  42603  sticksstones6  42604  sticksstones7  42605  sticksstones10  42608  sticksstones11  42609  sticksstones12a  42610  sticksstones12  42611  sticksstones22  42621  aks6d1c6lem3  42625  bcled  42631  bcle2d  42632  aks6d1c7lem1  42633  aks6d1c7lem2  42634  grpods  42647  unitscyglem2  42649  unitscyglem4  42651  aks5lem8  42654  sumcubes  42759  gcdle1d  42776  gcdle2d  42777  frlmvscadiccat  42965  fltdiv  43083  flt4lem4  43096  fltnltalem  43109  eldioph2lem1  43206  pellexlem5  43279  congrep  43419  jm2.18  43434  jm2.19lem1  43435  jm2.19lem2  43436  jm2.19  43439  jm2.22  43441  jm2.23  43442  jm2.20nn  43443  jm2.25  43445  jm2.26a  43446  jm2.26lem3  43447  jm2.26  43448  jm2.27a  43451  jm2.27b  43452  jm2.27c  43453  jm3.1  43466  expdiophlem1  43467  hbtlem5  43574  radcnvrat  44759  nzin  44763  bccbc  44790  binomcxplemnn0  44794  binomcxplemnotnn0  44801  fprodexp  46042  mccllem  46045  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvnxpaek  46388  dvnmul  46389  dvnprodlem1  46392  dvnprodlem2  46393  wallispilem1  46511  wallispilem5  46515  stirlinglem3  46522  stirlinglem5  46524  stirlinglem7  46526  stirlinglem8  46527  fourierdlem102  46654  fourierdlem114  46666  sqwvfoura  46674  elaa2lem  46679  etransclem10  46690  etransclem20  46700  etransclem21  46701  etransclem22  46702  etransclem23  46703  etransclem24  46704  etransclem27  46707  etransclem28  46708  etransclem35  46715  etransclem38  46718  etransclem44  46724  etransclem45  46725  etransclem46  46726  sge0ad2en  46877  chnsubseqwl  47325  chnsubseq  47326  fsummmodsnunz  47843  fmtnoge3  48005  fmtnof1  48010  fmtnorec1  48012  sqrtpwpw2p  48013  fmtnodvds  48019  goldbachthlem2  48021  fmtnoprmfac2lem1  48041  lighneallem3  48082  lighneallem4b  48084  lighneallem4  48085  ssnn0ssfz  48837  altgsumbcALT  48841  flnn0ohalf  49022  dig2nn1st  49093  0dig2nn0o  49101  aacllem  50288