Theorem nn0zd 12612

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

Syntax hints:   → wi 4   ∈ wcel 2149  ℕ₀cn0 12500  ℤcz 12587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402  ax-un 7730  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-i2m1 11164  ax-1ne0 11165  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6300  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-ov 7411  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-neg 11440  df-nn 12230  df-n0 12501  df-z 12588

This theorem is referenced by:  nnzd  12613  eluzmn  12865  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  16090  binomrisefac  16092  fallfacval4  16093  bpolydiflem  16104  ruclem10  16291  sumodd  16442  divalglem9  16455  divalgmod  16460  bitsfzolem  16488  bitsfzo  16489  bitsmod  16490  bitsfi  16491  bitsinv1lem  16495  sadcaddlem  16511  sadadd3  16515  sadaddlem  16520  sadadd  16521  sadasslem  16524  sadass  16525  sadeq  16526  bitsres  16527  bitsuz  16528  bitsshft  16529  smuval2  16536  smupvallem  16537  smupval  16542  smueqlem  16544  smumullem  16546  smumul  16547  gcdcllem1  16553  zeqzmulgcd  16564  gcd0id  16573  gcdneg  16576  modgcd  16586  gcdmultipled  16588  bezoutlem4  16596  dvdsgcdb  16599  gcdass  16601  mulgcd  16602  gcdzeq  16606  dvdsmulgcd  16610  bezoutr  16622  bezoutr1  16623  nn0seqcvgd  16624  algfx  16634  eucalginv  16638  eucalg  16641  gcddvdslcm  16656  lcmneg  16657  lcmgcdlem  16660  lcmdvds  16662  lcmgcdeq  16666  lcmdvdsb  16667  lcmass  16668  lcmftp  16690  lcmfunsnlem1  16691  lcmfunsnlem2lem1  16692  lcmfunsnlem2lem2  16693  lcmfunsnlem2  16694  lcmfdvdsb  16697  lcmfun  16699  lcmfass  16700  mulgcddvds  16709  rpmulgcd2  16710  qredeu  16712  divgcdcoprm0  16719  sqnprm  16757  prmdvdsbc  16781  divnumden  16803  powm2modprm  16859  coprimeprodsq  16864  iserodd  16891  pclem  16894  pcpre1  16898  pcpremul  16899  pcqcl  16912  pcdvdsb  16925  pcidlem  16928  pc2dvds  16935  pcprmpw2  16938  dvdsprmpweqle  16942  pcadd  16945  pcfac  16955  pcbc  16956  pockthlem  16961  prmreclem2  16973  prmreclem3  16974  mul4sqlem  17009  4sqlem11  17011  4sqlem12  17012  4sqlem14  17014  vdwapun  17030  prmgaplcmlem1  17107  chnind  18673  chnub  18674  chnpolfz  18685  lagsubg  19262  psgnuni  19565  psgnran  19581  odmodnn0  19606  mndodconglem  19607  mndodcong  19608  odm1inv  19619  odmulg2  19621  odmulg  19622  odmulgeq  19623  odbezout  19624  odinv  19627  odf1  19628  gexod  19652  gexdvds3  19656  sylow1lem1  19664  sylow1lem3  19666  pgpfi  19671  pgpssslw  19680  sylow2alem2  19684  sylow2blem3  19688  fislw  19691  sylow3lem4  19696  sylow3lem6  19698  efginvrel2  19793  efgredlemf  19807  efgredlemd  19810  efgredlemc  19811  efgredlem  19813  efgcpbllemb  19821  odadd1  19914  odadd2  19915  gexexlem  19918  gexex  19919  torsubg  19920  lt6abl  19961  gsummulg  20008  ablfacrplem  20133  ablfacrp  20134  ablfacrp2  20135  ablfac1b  20138  ablfac1c  20139  ablfac1eulem  20140  ablfac1eu  20141  pgpfac1lem2  20143  pgpfaclem1  20149  ablfaclem3  20155  srgbinomlem3  20306  srgbinomlem4  20307  chrid  21640  znunit  21678  freshmansdream  21689  psgnghm  21695  asclmulg  22017  psrbaglefi  22041  psdvsca  22292  psdmul  22294  chfacfscmulfsupp  22981  chfacfpmmulfsupp  22985  cpmadugsumlemF  22998  dyadss  25718  dyaddisjlem  25719  ply1divex  26259  ply1termlem  26325  plyeq0lem  26332  plyaddlem1  26335  plymullem1  26336  coeeulem  26346  coeidlem  26359  coeeq2  26364  coemulhi  26376  dvply1  26410  dvply2g  26411  plydivex  26423  elqaalem2  26446  aareccl  26452  aannenlem1  26454  aalioulem1  26458  taylplem1  26488  taylplem2  26489  taylpfval  26490  dvtaylp  26495  taylthlem2  26499  dvradcnv  26546  abelthlem7  26563  cxpeq  26884  birthdaylem2  27079  ftalem1  27199  basellem3  27209  isppw2  27241  isnsqf  27261  mule1  27274  ppinncl  27300  musum  27317  chtublem  27337  pclogsum  27341  vmasum  27342  dchrabs  27386  bcmax  27404  bposlem1  27410  bposlem6  27415  lgsval2lem  27433  lgsmod  27449  lgsne0  27461  gausslemma2dlem0h  27489  gausslemma2dlem0i  27490  gausslemma2dlem2  27493  gausslemma2dlem6  27498  gausslemma2d  27500  lgseisenlem1  27501  lgseisenlem2  27502  lgseisenlem3  27503  lgseisenlem4  27504  lgsquadlem1  27506  m1lgs  27514  2lgslem1a  27517  2lgslem3a  27522  2lgslem3b  27523  2lgslem3c  27524  2lgslem3d  27525  2lgslem3d1  27529  2lgsoddprmlem2  27535  2sqlem8  27552  2sqcoprm  27561  2sqmod  27562  chebbnd1lem1  27595  dchrisumlem1  27615  dchrisum0flblem1  27634  selberg2lem  27676  ostth2lem2  27760  ostth2lem3  27761  finsumvtxdg2sstep  29836  finsumvtxdgeven  29839  vtxdgoddnumeven  29840  redwlklem  29956  wlkdlem1  29967  pthdlem1  30052  crctcshwlkn0lem4  30099  wwlksnredwwlkn0  30182  wwlksnextproplem2  30196  clwwlkccatlem  30277  clwlkclwwlkfo  30297  clwwlkwwlksb  30342  clwwlkndivn  30368  eupth2lem3lem3  30518  eupth2lem3lem4  30519  eupth2lem3  30524  eupth2lems  30526  numclwwlk5  30676  numclwwlk6  30678  ex-ind-dvds  30749  nndiffz1  33068  fzo0opth  33085  ccatf1  33206  pfxlsw2ccat  33207  wrdt2ind  33210  gsummulsubdishift1  33325  gsumwrd2dccatlem  33334  cycpmfv1  33370  cycpmco2lem2  33384  cycpmco2lem3  33385  cycpmco2lem4  33386  cycpmco2lem5  33387  cycpmco2lem6  33388  cycpmco2  33390  cycpmrn  33400  cyc3genpm  33409  cycpmconjslem2  33412  cyc3conja  33414  archirng  33445  archirngz  33446  archiabllem1a  33448  gsumind  33604  elrspunidl  33676  ply1coedeg  33820  ply1degltel  33825  gsummoncoe1fz  33829  selvply1rhmlemb  33850  esplyfval2  33896  esplympl  33898  esplyfval3  33903  esplyindfv  33907  vietalem  33910  ply1degltdimlem  33953  fldextrspundgdvds  34012  algextdeglem8  34055  rtelextdg2  34058  constrext2chnlem  34081  cos9thpiminplylem2  34114  cos9thpiminplylem3  34115  cos9thpiminplylem6  34118  cos9thpiminply  34119  madjusmdetlem4  34161  zrhcntr  34310  qqhval2lem  34312  oddpwdc  34685  eulerpartlems  34691  eulerpartlemb  34699  sseqfv1  34720  sseqfn  34721  sseqmw  34722  sseqf  34723  sseqfv2  34725  sseqp1  34726  ccatmulgnn0dir  34873  signsplypnf  34878  signsply0  34879  signslema  34890  signstfvn  34897  signstfvp  34899  signstfvc  34902  fsum2dsub  34935  reprinfz1  34950  reprfi2  34951  hashrepr  34953  reprdifc  34955  breprexplema  34958  breprexplemc  34960  circlemeth  34968  circlevma  34970  circlemethhgt  34971  hgt750lema  34985  tgoldbachgtde  34988  lpadlem3  35009  revpfxsfxrev  35502  revwlk  35512  subfacval3  35576  bcprod  36125  bccolsum  36126  fwddifnp1  36552  knoppndvlem6  36991  knoppndvlem7  36992  knoppndvlem10  36995  knoppndvlem14  36999  knoppndvlem15  37000  knoppndvlem16  37001  knoppndvlem17  37002  knoppndvlem19  37004  knoppndvlem21  37006  dfgcd3  37851  poimirlem3  38157  poimirlem4  38158  poimirlem6  38160  poimirlem13  38167  poimirlem14  38168  poimirlem17  38171  poimirlem21  38175  poimirlem22  38176  poimirlem23  38177  poimirlem26  38180  poimirlem27  38181  poimirlem31  38185  geomcau  38293  bccl2d  42643  lcmineqlem12  42692  lcmineqlem17  42697  dvrelogpow2b  42720  aks4d1p1p2  42722  aks4d1p1p4  42723  aks4d1p1p6  42725  aks4d1p1p7  42726  aks4d1p1p5  42727  aks4d1p1  42728  aks4d1p3  42730  aks4d1p6  42733  aks4d1p8d2  42737  aks4d1p8d3  42738  aks4d1p8  42739  primrootscoprmpow  42751  primrootlekpowne0  42757  aks6d1c1  42768  aks6d1c2p2  42771  aks6d1c2lem4  42779  aks6d1c2  42782  aks6d1c5lem3  42789  aks6d1c5lem2  42790  2np3bcnp1  42796  sticksstones5  42802  sticksstones6  42803  sticksstones7  42804  sticksstones10  42807  sticksstones11  42808  sticksstones12a  42809  sticksstones12  42810  sticksstones22  42820  aks6d1c6lem3  42824  bcled  42830  bcle2d  42831  aks6d1c7lem1  42832  aks6d1c7lem2  42833  grpods  42846  unitscyglem2  42848  unitscyglem4  42850  aks5lem8  42853  sumcubes  42959  gcdle1d  42976  gcdle2d  42977  frlmvscadiccat  43165  fltdiv  43255  flt4lem4  43268  fltnltalem  43281  eldioph2lem1  43378  pellexlem5  43447  congrep  43587  jm2.18  43602  jm2.19lem1  43603  jm2.19lem2  43604  jm2.19  43607  jm2.22  43609  jm2.23  43610  jm2.20nn  43611  jm2.25  43613  jm2.26a  43614  jm2.26lem3  43615  jm2.26  43616  jm2.27a  43619  jm2.27b  43620  jm2.27c  43621  jm3.1  43634  expdiophlem1  43635  hbtlem5  43742  radcnvrat  44911  nzin  44915  bccbc  44942  binomcxplemnn0  44946  binomcxplemnotnn0  44953  fprodexp  46197  mccllem  46200  ioodvbdlimc1lem2  46533  ioodvbdlimc2lem  46535  dvnxpaek  46543  dvnmul  46544  dvnprodlem1  46547  dvnprodlem2  46548  wallispilem1  46666  wallispilem5  46670  stirlinglem3  46677  stirlinglem5  46679  stirlinglem7  46681  stirlinglem8  46682  fourierdlem102  46809  fourierdlem114  46821  sqwvfoura  46829  elaa2lem  46834  etransclem10  46845  etransclem20  46855  etransclem21  46856  etransclem22  46857  etransclem23  46858  etransclem24  46859  etransclem27  46862  etransclem28  46863  etransclem35  46870  etransclem38  46873  etransclem44  46879  etransclem45  46880  etransclem46  46881  sge0ad2en  47032  chnsubseqwl  47482  chnsubseq  47483  fsummmodsnunz  48004  fmtnoge3  48166  fmtnof1  48171  fmtnorec1  48173  sqrtpwpw2p  48174  fmtnodvds  48180  goldbachthlem2  48182  fmtnoprmfac2lem1  48202  lighneallem3  48243  lighneallem4b  48245  lighneallem4  48246  ssnn0ssfz  49009  altgsumbcALT  49013  flnn0ohalf  49194  dig2nn1st  49265  0dig2nn0o  49273  aacllem  50470