Theorem nn0zd 12504

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℕ₀cn0 12392  ℤcz 12479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7677  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-addrcl 11078  ax-mulcl 11079  ax-mulrcl 11080  ax-i2m1 11085  ax-1ne0 11086  ax-rnegex 11088  ax-rrecex 11089  ax-cnre 11090

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7358  df-om 7806  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-neg 11358  df-nn 12137  df-n0 12393  df-z 12480

This theorem is referenced by:  nnzd  12505  eluzmn  12749  difelfznle  13549  elfzodif0  13677  zmodfz  13804  expnegz  14010  expaddzlem  14019  expaddz  14020  expmulz  14022  faclbnd  14204  bcpasc  14235  hashf1  14371  fz1isolem  14375  hashge2el2dif  14394  hashtpg  14399  wrdffz  14449  ffz0iswrd  14455  wrdsymb0  14463  wrdlenge1n0  14464  ccatcl  14488  ccatval3  14493  ccatdmss  14496  ccatsymb  14497  ccatval21sw  14500  ccatass  14503  ccatrn  14504  lswccatn0lsw  14506  ccats1val2  14542  swrdnd  14569  swrdccat2  14584  pfxtrcfv0  14608  pfxtrcfvl  14611  pfxccat1  14616  swrdccatin2  14643  pfxccatin12  14647  pfxccatpfx2  14651  pfxccat3a  14652  splfv2a  14670  splval2  14671  revcl  14675  revccat  14680  revrev  14681  cshwmodn  14709  cshwsublen  14710  cshwn  14711  cshwidxmod  14717  2cshwid  14728  3cshw  14732  cshweqdif2  14733  revco  14748  ccatco  14749  ccat2s1fvwALT  14869  ofccat  14883  zabscl  15227  absrdbnd  15256  iseraltlem3  15598  fsum0diaglem  15690  modfsummods  15707  binomlem  15743  binom1p  15745  incexc2  15752  climcndslem1  15763  geoser  15781  pwm1geoser  15783  geolim2  15785  mertenslem1  15798  mertenslem2  15799  mertens  15800  binomfallfaclem2  15954  binomrisefac  15956  fallfacval4  15957  bpolydiflem  15968  ruclem10  16155  sumodd  16306  divalglem9  16319  divalgmod  16324  bitsfzolem  16352  bitsfzo  16353  bitsmod  16354  bitsfi  16355  bitsinv1lem  16359  sadcaddlem  16375  sadadd3  16379  sadaddlem  16384  sadadd  16385  sadasslem  16388  sadass  16389  sadeq  16390  bitsres  16391  bitsuz  16392  bitsshft  16393  smuval2  16400  smupvallem  16401  smupval  16406  smueqlem  16408  smumullem  16410  smumul  16411  gcdcllem1  16417  zeqzmulgcd  16428  gcd0id  16437  gcdneg  16440  modgcd  16450  gcdmultipled  16452  bezoutlem4  16460  dvdsgcdb  16463  gcdass  16465  mulgcd  16466  gcdzeq  16470  dvdsmulgcd  16474  bezoutr  16486  bezoutr1  16487  nn0seqcvgd  16488  algfx  16498  eucalginv  16502  eucalg  16505  gcddvdslcm  16520  lcmneg  16521  lcmgcdlem  16524  lcmdvds  16526  lcmgcdeq  16530  lcmdvdsb  16531  lcmass  16532  lcmftp  16554  lcmfunsnlem1  16555  lcmfunsnlem2lem1  16556  lcmfunsnlem2lem2  16557  lcmfunsnlem2  16558  lcmfdvdsb  16561  lcmfun  16563  lcmfass  16564  mulgcddvds  16573  rpmulgcd2  16574  qredeu  16576  divgcdcoprm0  16583  sqnprm  16620  prmdvdsbc  16644  divnumden  16666  powm2modprm  16722  coprimeprodsq  16727  iserodd  16754  pclem  16757  pcpre1  16761  pcpremul  16762  pcqcl  16775  pcdvdsb  16788  pcidlem  16791  pc2dvds  16798  pcprmpw2  16801  dvdsprmpweqle  16805  pcadd  16808  pcfac  16818  pcbc  16819  pockthlem  16824  prmreclem2  16836  prmreclem3  16837  mul4sqlem  16872  4sqlem11  16874  4sqlem12  16875  4sqlem14  16877  vdwapun  16893  prmgaplcmlem1  16970  chnind  18535  chnub  18536  chnpolfz  18547  lagsubg  19115  psgnuni  19419  psgnran  19435  odmodnn0  19460  mndodconglem  19461  mndodcong  19462  odm1inv  19473  odmulg2  19475  odmulg  19476  odmulgeq  19477  odbezout  19478  odinv  19481  odf1  19482  gexod  19506  gexdvds3  19510  sylow1lem1  19518  sylow1lem3  19520  pgpfi  19525  pgpssslw  19534  sylow2alem2  19538  sylow2blem3  19542  fislw  19545  sylow3lem4  19550  sylow3lem6  19552  efginvrel2  19647  efgredlemf  19661  efgredlemd  19664  efgredlemc  19665  efgredlem  19667  efgcpbllemb  19675  odadd1  19768  odadd2  19769  gexexlem  19772  gexex  19773  torsubg  19774  lt6abl  19815  gsummulg  19862  ablfacrplem  19987  ablfacrp  19988  ablfacrp2  19989  ablfac1b  19992  ablfac1c  19993  ablfac1eulem  19994  ablfac1eu  19995  pgpfac1lem2  19997  pgpfaclem1  20003  ablfaclem3  20009  srgbinomlem3  20154  srgbinomlem4  20155  chrid  21471  znunit  21509  freshmansdream  21520  psgnghm  21526  asclmulg  21849  psrbaglefi  21873  psdvsca  22098  psdmul  22100  chfacfscmulfsupp  22794  chfacfpmmulfsupp  22798  cpmadugsumlemF  22811  dyadss  25542  dyaddisjlem  25543  ply1divex  26089  ply1termlem  26155  plyeq0lem  26162  plyaddlem1  26165  plymullem1  26166  coeeulem  26176  coeidlem  26189  coeeq2  26194  coemulhi  26206  dvply1  26238  dvply2g  26239  dvply2gOLD  26240  plydivex  26252  elqaalem2  26275  aareccl  26281  aannenlem1  26283  aalioulem1  26287  taylplem1  26317  taylplem2  26318  taylpfval  26319  dvtaylp  26325  taylthlem2  26329  taylthlem2OLD  26330  dvradcnv  26377  abelthlem7  26395  cxpeq  26714  birthdaylem2  26909  ftalem1  27030  basellem3  27040  isppw2  27072  isnsqf  27092  mule1  27105  ppinncl  27131  musum  27148  chtublem  27169  pclogsum  27173  vmasum  27174  dchrabs  27218  bcmax  27236  bposlem1  27242  bposlem6  27247  lgsval2lem  27265  lgsmod  27281  lgsne0  27293  gausslemma2dlem0h  27321  gausslemma2dlem0i  27322  gausslemma2dlem2  27325  gausslemma2dlem6  27330  gausslemma2d  27332  lgseisenlem1  27333  lgseisenlem2  27334  lgseisenlem3  27335  lgseisenlem4  27336  lgsquadlem1  27338  m1lgs  27346  2lgslem1a  27349  2lgslem3a  27354  2lgslem3b  27355  2lgslem3c  27356  2lgslem3d  27357  2lgslem3d1  27361  2lgsoddprmlem2  27367  2sqlem8  27384  2sqcoprm  27393  2sqmod  27394  chebbnd1lem1  27427  dchrisumlem1  27447  dchrisum0flblem1  27466  selberg2lem  27508  ostth2lem2  27592  ostth2lem3  27593  finsumvtxdg2sstep  29549  finsumvtxdgeven  29552  vtxdgoddnumeven  29553  redwlklem  29669  wlkdlem1  29680  pthdlem1  29765  crctcshwlkn0lem4  29812  wwlksnredwwlkn0  29895  wwlksnextproplem2  29909  clwwlkccatlem  29990  clwlkclwwlkfo  30010  clwwlkwwlksb  30055  clwwlkndivn  30081  eupth2lem3lem3  30231  eupth2lem3lem4  30232  eupth2lem3  30237  eupth2lems  30239  numclwwlk5  30389  numclwwlk6  30391  ex-ind-dvds  30462  nndiffz1  32794  fzo0opth  32811  ccatf1  32959  pfxlsw2ccat  32960  wrdt2ind  32963  gsummulsubdishift1  33079  gsumwrd2dccatlem  33087  cycpmfv1  33123  cycpmco2lem2  33137  cycpmco2lem3  33138  cycpmco2lem4  33139  cycpmco2lem5  33140  cycpmco2lem6  33141  cycpmco2  33143  cycpmrn  33153  cyc3genpm  33162  cycpmconjslem2  33165  cyc3conja  33167  archirng  33198  archirngz  33199  archiabllem1a  33201  gsumind  33354  elrspunidl  33437  ply1coedeg  33598  ply1degltel  33603  gsummoncoe1fz  33607  esplyfval2  33651  esplympl  33653  esplyfval3  33658  esplyindfv  33660  vietalem  33663  ply1degltdimlem  33707  fldextrspundgdvds  33766  algextdeglem8  33809  rtelextdg2  33812  constrext2chnlem  33835  cos9thpiminplylem2  33868  cos9thpiminplylem3  33869  cos9thpiminplylem6  33872  cos9thpiminply  33873  madjusmdetlem4  33915  zrhcntr  34064  qqhval2lem  34066  oddpwdc  34439  eulerpartlems  34445  eulerpartlemb  34453  sseqfv1  34474  sseqfn  34475  sseqmw  34476  sseqf  34477  sseqfv2  34479  sseqp1  34480  ccatmulgnn0dir  34627  signsplypnf  34635  signsply0  34636  signslema  34647  signstfvn  34654  signstfvp  34656  signstfvc  34659  fsum2dsub  34692  reprinfz1  34707  reprfi2  34708  hashrepr  34710  reprdifc  34712  breprexplema  34715  breprexplemc  34717  circlemeth  34725  circlevma  34727  circlemethhgt  34728  hgt750lema  34742  tgoldbachgtde  34745  lpadlem3  34763  revpfxsfxrev  35232  revwlk  35241  subfacval3  35305  bcprod  35854  bccolsum  35855  fwddifnp1  36281  knoppndvlem6  36633  knoppndvlem7  36634  knoppndvlem10  36637  knoppndvlem14  36641  knoppndvlem15  36642  knoppndvlem16  36643  knoppndvlem17  36644  knoppndvlem19  36646  knoppndvlem21  36648  dfgcd3  37441  poimirlem3  37736  poimirlem4  37737  poimirlem6  37739  poimirlem13  37746  poimirlem14  37747  poimirlem17  37750  poimirlem21  37754  poimirlem22  37755  poimirlem23  37756  poimirlem26  37759  poimirlem27  37760  poimirlem31  37764  geomcau  37872  bccl2d  42157  lcmineqlem12  42206  lcmineqlem17  42211  dvrelogpow2b  42234  aks4d1p1p2  42236  aks4d1p1p4  42237  aks4d1p1p6  42239  aks4d1p1p7  42240  aks4d1p1p5  42241  aks4d1p1  42242  aks4d1p3  42244  aks4d1p6  42247  aks4d1p8d2  42251  aks4d1p8d3  42252  aks4d1p8  42253  primrootscoprmpow  42265  primrootlekpowne0  42271  aks6d1c1  42282  aks6d1c2p2  42285  aks6d1c2lem4  42293  aks6d1c2  42296  aks6d1c5lem3  42303  aks6d1c5lem2  42304  2np3bcnp1  42310  sticksstones5  42316  sticksstones6  42317  sticksstones7  42318  sticksstones10  42321  sticksstones11  42322  sticksstones12a  42323  sticksstones12  42324  sticksstones22  42334  aks6d1c6lem3  42338  bcled  42344  bcle2d  42345  aks6d1c7lem1  42346  aks6d1c7lem2  42347  grpods  42360  unitscyglem2  42362  unitscyglem4  42364  aks5lem8  42367  sumcubes  42483  gcdle1d  42500  gcdle2d  42501  frlmvscadiccat  42676  fltdiv  42794  flt4lem4  42807  fltnltalem  42820  eldioph2lem1  42917  pellexlem5  42990  congrep  43130  jm2.18  43145  jm2.19lem1  43146  jm2.19lem2  43147  jm2.19  43150  jm2.22  43152  jm2.23  43153  jm2.20nn  43154  jm2.25  43156  jm2.26a  43157  jm2.26lem3  43158  jm2.26  43159  jm2.27a  43162  jm2.27b  43163  jm2.27c  43164  jm3.1  43177  expdiophlem1  43178  hbtlem5  43285  radcnvrat  44471  nzin  44475  bccbc  44502  binomcxplemnn0  44506  binomcxplemnotnn0  44513  fprodexp  45756  mccllem  45759  ioodvbdlimc1lem2  46092  ioodvbdlimc2lem  46094  dvnxpaek  46102  dvnmul  46103  dvnprodlem1  46106  dvnprodlem2  46107  wallispilem1  46225  wallispilem5  46229  stirlinglem3  46236  stirlinglem5  46238  stirlinglem7  46240  stirlinglem8  46241  fourierdlem102  46368  fourierdlem114  46380  sqwvfoura  46388  elaa2lem  46393  etransclem10  46404  etransclem20  46414  etransclem21  46415  etransclem22  46416  etransclem23  46417  etransclem24  46418  etransclem27  46421  etransclem28  46422  etransclem35  46429  etransclem38  46432  etransclem44  46438  etransclem45  46439  etransclem46  46440  sge0ad2en  46591  chnsubseqwl  47039  chnsubseq  47040  fsummmodsnunz  47537  fmtnoge3  47692  fmtnof1  47697  fmtnorec1  47699  sqrtpwpw2p  47700  fmtnodvds  47706  goldbachthlem2  47708  fmtnoprmfac2lem1  47728  lighneallem3  47769  lighneallem4b  47771  lighneallem4  47772  ssnn0ssfz  48511  altgsumbcALT  48515  flnn0ohalf  48696  dig2nn1st  48767  0dig2nn0o  48775  aacllem  49962