Theorem nn0zd 12611

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℕ₀cn0 12499  ℤcz 12586

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-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-i2m1 11163  ax-1ne0 11164  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-neg 11439  df-nn 12229  df-n0 12500  df-z 12587

This theorem is referenced by:  nnzd  12612  eluzmn  12864  difelfznle  13666  elfzodif0  13795  zmodfz  13922  expnegz  14128  expaddzlem  14137  expaddz  14138  expmulz  14140  faclbnd  14322  bcpasc  14353  hashf1  14490  fz1isolem  14494  hashge2el2dif  14513  hashtpg  14518  wrdffz  14568  ffz0iswrd  14574  wrdsymb0  14582  wrdlenge1n0  14583  ccatcl  14607  ccatval3  14612  ccatdmss  14615  ccatsymb  14616  ccatval21sw  14619  ccatass  14622  ccatrn  14623  lswccatn0lsw  14625  ccats1val2  14661  swrdnd  14688  swrdccat2  14703  pfxtrcfv0  14727  pfxtrcfvl  14730  pfxccat1  14735  swrdccatin2  14762  pfxccatin12  14766  pfxccatpfx2  14770  pfxccat3a  14771  splfv2a  14789  splval2  14790  revcl  14794  revccat  14799  revrev  14800  cshwmodn  14828  cshwsublen  14829  cshwn  14830  cshwidxmod  14836  2cshwid  14847  3cshw  14851  cshweqdif2  14852  revco  14867  ccatco  14868  ccat2s1fvwALT  14988  ofccat  15002  zabscl  15360  absrdbnd  15389  iseraltlem3  15731  fsum0diaglem  15823  modfsummods  15841  binomlem  15879  binom1p  15881  incexc2  15888  climcndslem1  15899  geoser  15917  pwm1geoser  15919  geolim2  15921  mertenslem1  15934  mertenslem2  15935  mertens  15936  binomfallfaclem2  16089  binomrisefac  16091  fallfacval4  16092  bpolydiflem  16103  ruclem10  16290  sumodd  16441  divalglem9  16454  divalgmod  16459  bitsfzolem  16487  bitsfzo  16488  bitsmod  16489  bitsfi  16490  bitsinv1lem  16494  sadcaddlem  16510  sadadd3  16514  sadaddlem  16519  sadadd  16520  sadasslem  16523  sadass  16524  sadeq  16525  bitsres  16526  bitsuz  16527  bitsshft  16528  smuval2  16535  smupvallem  16536  smupval  16541  smueqlem  16543  smumullem  16545  smumul  16546  gcdcllem1  16552  zeqzmulgcd  16563  gcd0id  16572  gcdneg  16575  modgcd  16585  gcdmultipled  16587  bezoutlem4  16595  dvdsgcdb  16598  gcdass  16600  mulgcd  16601  gcdzeq  16605  dvdsmulgcd  16609  bezoutr  16621  bezoutr1  16622  nn0seqcvgd  16623  algfx  16633  eucalginv  16637  eucalg  16640  gcddvdslcm  16655  lcmneg  16656  lcmgcdlem  16659  lcmdvds  16661  lcmgcdeq  16665  lcmdvdsb  16666  lcmass  16667  lcmftp  16689  lcmfunsnlem1  16690  lcmfunsnlem2lem1  16691  lcmfunsnlem2lem2  16692  lcmfunsnlem2  16693  lcmfdvdsb  16696  lcmfun  16698  lcmfass  16699  mulgcddvds  16708  rpmulgcd2  16709  qredeu  16711  divgcdcoprm0  16718  sqnprm  16756  prmdvdsbc  16780  divnumden  16802  powm2modprm  16858  coprimeprodsq  16863  iserodd  16890  pclem  16893  pcpre1  16897  pcpremul  16898  pcqcl  16911  pcdvdsb  16924  pcidlem  16927  pc2dvds  16934  pcprmpw2  16937  dvdsprmpweqle  16941  pcadd  16944  pcfac  16954  pcbc  16955  pockthlem  16960  prmreclem2  16972  prmreclem3  16973  mul4sqlem  17008  4sqlem11  17010  4sqlem12  17011  4sqlem14  17013  vdwapun  17029  prmgaplcmlem1  17106  chnind  18672  chnub  18673  chnpolfz  18684  lagsubg  19261  psgnuni  19564  psgnran  19580  odmodnn0  19605  mndodconglem  19606  mndodcong  19607  odm1inv  19618  odmulg2  19620  odmulg  19621  odmulgeq  19622  odbezout  19623  odinv  19626  odf1  19627  gexod  19651  gexdvds3  19655  sylow1lem1  19663  sylow1lem3  19665  pgpfi  19670  pgpssslw  19679  sylow2alem2  19683  sylow2blem3  19687  fislw  19690  sylow3lem4  19695  sylow3lem6  19697  efginvrel2  19792  efgredlemf  19806  efgredlemd  19809  efgredlemc  19810  efgredlem  19812  efgcpbllemb  19820  odadd1  19913  odadd2  19914  gexexlem  19917  gexex  19918  torsubg  19919  lt6abl  19960  gsummulg  20007  ablfacrplem  20132  ablfacrp  20133  ablfacrp2  20134  ablfac1b  20137  ablfac1c  20138  ablfac1eulem  20139  ablfac1eu  20140  pgpfac1lem2  20142  pgpfaclem1  20148  ablfaclem3  20154  srgbinomlem3  20305  srgbinomlem4  20306  chrid  21675  znunit  21713  freshmansdream  21724  psgnghm  21730  asclmulg  22052  psrbaglefi  22076  psdvsca  22327  psdmul  22329  chfacfscmulfsupp  23016  chfacfpmmulfsupp  23020  cpmadugsumlemF  23033  dyadss  25753  dyaddisjlem  25754  ply1divex  26294  ply1termlem  26360  plyeq0lem  26367  plyaddlem1  26370  plymullem1  26371  coeeulem  26381  coeidlem  26394  coeeq2  26399  coemulhi  26411  dvply1  26445  dvply2g  26446  plydivex  26458  elqaalem2  26481  aareccl  26489  aannenlem1  26491  aalioulem1  26495  taylplem1  26526  taylplem2  26527  taylpfval  26528  dvtaylp  26533  taylthlem2  26537  dvradcnv  26584  abelthlem7  26601  cxpeq  26922  birthdaylem2  27117  ftalem1  27237  basellem3  27247  isppw2  27279  isnsqf  27299  mule1  27312  ppinncl  27338  musum  27355  chtublem  27375  pclogsum  27379  vmasum  27380  dchrabs  27424  bcmax  27442  bposlem1  27448  bposlem6  27453  lgsval2lem  27471  lgsmod  27487  lgsne0  27499  gausslemma2dlem0h  27527  gausslemma2dlem0i  27528  gausslemma2dlem2  27531  gausslemma2dlem6  27536  gausslemma2d  27538  lgseisenlem1  27539  lgseisenlem2  27540  lgseisenlem3  27541  lgseisenlem4  27542  lgsquadlem1  27544  m1lgs  27552  2lgslem1a  27555  2lgslem3a  27560  2lgslem3b  27561  2lgslem3c  27562  2lgslem3d  27563  2lgslem3d1  27567  2lgsoddprmlem2  27573  2sqlem8  27590  2sqcoprm  27599  2sqmod  27600  chebbnd1lem1  27633  dchrisumlem1  27653  dchrisum0flblem1  27672  selberg2lem  27714  ostth2lem2  27798  ostth2lem3  27799  finsumvtxdg2sstep  29899  finsumvtxdgeven  29902  vtxdgoddnumeven  29903  redwlklem  30019  wlkdlem1  30030  pthdlem1  30115  crctcshwlkn0lem4  30162  wwlksnredwwlkn0  30245  wwlksnextproplem2  30259  clwwlkccatlem  30340  clwlkclwwlkfo  30360  clwwlkwwlksb  30405  clwwlkndivn  30431  eupth2lem3lem3  30581  eupth2lem3lem4  30582  eupth2lem3  30587  eupth2lems  30589  numclwwlk5  30739  numclwwlk6  30741  ex-ind-dvds  30812  nndiffz1  33131  fzo0opth  33148  ccatf1  33269  pfxlsw2ccat  33270  wrdt2ind  33273  gsummulsubdishift1  33388  gsumwrd2dccatlem  33397  cycpmfv1  33433  cycpmco2lem2  33447  cycpmco2lem3  33448  cycpmco2lem4  33449  cycpmco2lem5  33450  cycpmco2lem6  33451  cycpmco2  33453  cycpmrn  33463  cyc3genpm  33472  cycpmconjslem2  33475  cyc3conja  33477  archirng  33508  archirngz  33509  archiabllem1a  33511  gsumind  33665  elrspunidl  33736  ply1coedeg  33879  ply1degltel  33884  gsummoncoe1fz  33888  selvply1rhmlemb  33909  esplyfval2  33955  esplympl  33957  esplyfval3  33962  esplyindfv  33966  vietalem  33969  ply1degltdimlem  34012  fldextrspundgdvds  34071  algextdeglem8  34114  rtelextdg2  34117  constrext2chnlem  34140  cos9thpiminplylem2  34173  cos9thpiminplylem3  34174  cos9thpiminplylem6  34177  cos9thpiminply  34178  madjusmdetlem4  34220  zrhcntr  34369  qqhval2lem  34371  oddpwdc  34744  eulerpartlems  34750  eulerpartlemb  34758  sseqfv1  34779  sseqfn  34780  sseqmw  34781  sseqf  34782  sseqfv2  34784  sseqp1  34785  ccatmulgnn0dir  34932  signsplypnf  34937  signsply0  34938  signslema  34949  signstfvn  34956  signstfvp  34958  signstfvc  34961  fsum2dsub  34994  reprinfz1  35009  reprfi2  35010  hashrepr  35012  reprdifc  35014  breprexplema  35017  breprexplemc  35019  circlemeth  35027  circlevma  35029  circlemethhgt  35030  hgt750lema  35044  tgoldbachgtde  35047  lpadlem3  35068  revpfxsfxrev  35607  revwlk  35617  subfacval3  35681  bcprod  36230  bccolsum  36231  fwddifnp1  36657  knoppndvlem6  37106  knoppndvlem7  37107  knoppndvlem10  37110  knoppndvlem14  37114  knoppndvlem15  37115  knoppndvlem16  37116  knoppndvlem17  37117  knoppndvlem19  37119  knoppndvlem21  37121  dfgcd3  37968  poimirlem3  38274  poimirlem4  38275  poimirlem6  38277  poimirlem13  38284  poimirlem14  38285  poimirlem17  38288  poimirlem21  38292  poimirlem22  38293  poimirlem23  38294  poimirlem26  38297  poimirlem27  38298  poimirlem31  38302  geomcau  38410  bccl2d  42758  lcmineqlem12  42807  lcmineqlem17  42812  dvrelogpow2b  42835  aks4d1p1p2  42837  aks4d1p1p4  42838  aks4d1p1p6  42840  aks4d1p1p7  42841  aks4d1p1p5  42842  aks4d1p1  42843  aks4d1p3  42845  aks4d1p6  42848  aks4d1p8d2  42852  aks4d1p8d3  42853  aks4d1p8  42854  primrootscoprmpow  42866  primrootlekpowne0  42872  aks6d1c1  42883  aks6d1c2p2  42886  aks6d1c2lem4  42894  aks6d1c2  42897  aks6d1c5lem3  42904  aks6d1c5lem2  42905  2np3bcnp1  42911  sticksstones5  42917  sticksstones6  42918  sticksstones7  42919  sticksstones10  42922  sticksstones11  42923  sticksstones12a  42924  sticksstones12  42925  sticksstones22  42935  aks6d1c6lem3  42939  bcled  42945  bcle2d  42946  aks6d1c7lem1  42947  aks6d1c7lem2  42948  grpods  42961  unitscyglem2  42963  unitscyglem4  42965  aks5lem8  42968  sumcubes  43074  gcdle1d  43091  gcdle2d  43092  frlmvscadiccat  43280  fltdiv  43368  flt4lem4  43381  fltnltalem  43394  eldioph2lem1  43491  pellexlem5  43560  congrep  43700  jm2.18  43715  jm2.19lem1  43716  jm2.19lem2  43717  jm2.19  43720  jm2.22  43722  jm2.23  43723  jm2.20nn  43724  jm2.25  43726  jm2.26a  43727  jm2.26lem3  43728  jm2.26  43729  jm2.27a  43732  jm2.27b  43733  jm2.27c  43734  jm3.1  43747  expdiophlem1  43748  hbtlem5  43855  radcnvrat  45024  nzin  45028  bccbc  45055  binomcxplemnn0  45059  binomcxplemnotnn0  45066  fprodexp  46310  mccllem  46313  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  dvnxpaek  46656  dvnmul  46657  dvnprodlem1  46660  dvnprodlem2  46661  wallispilem1  46779  wallispilem5  46783  stirlinglem3  46790  stirlinglem5  46792  stirlinglem7  46794  stirlinglem8  46795  fourierdlem102  46922  fourierdlem114  46934  sqwvfoura  46942  elaa2lem  46947  etransclem10  46958  etransclem20  46968  etransclem21  46969  etransclem22  46970  etransclem23  46971  etransclem24  46972  etransclem27  46975  etransclem28  46976  etransclem35  46983  etransclem38  46986  etransclem44  46992  etransclem45  46993  etransclem46  46994  sge0ad2en  47145  chnsubseqwl  47595  chnsubseq  47596  fsummmodsnunz  48120  fmtnoge3  48282  fmtnof1  48287  fmtnorec1  48289  sqrtpwpw2p  48290  fmtnodvds  48296  goldbachthlem2  48298  fmtnoprmfac2lem1  48318  lighneallem3  48359  lighneallem4b  48361  lighneallem4  48362  ssnn0ssfz  49129  altgsumbcALT  49133  flnn0ohalf  49314  dig2nn1st  49385  0dig2nn0o  49393  aacllem  50621