Theorem nn0zd 12525

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕ₀cn0 12413  ℤcz 12500

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 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111

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 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-neg 11379  df-nn 12158  df-n0 12414  df-z 12501

This theorem is referenced by:  nnzd  12526  eluzmn  12770  difelfznle  13570  elfzodif0  13698  zmodfz  13825  expnegz  14031  expaddzlem  14040  expaddz  14041  expmulz  14043  faclbnd  14225  bcpasc  14256  hashf1  14392  fz1isolem  14396  hashge2el2dif  14415  hashtpg  14420  wrdffz  14470  ffz0iswrd  14476  wrdsymb0  14484  wrdlenge1n0  14485  ccatcl  14509  ccatval3  14514  ccatdmss  14517  ccatsymb  14518  ccatval21sw  14521  ccatass  14524  ccatrn  14525  lswccatn0lsw  14527  ccats1val2  14563  swrdnd  14590  swrdccat2  14605  pfxtrcfv0  14629  pfxtrcfvl  14632  pfxccat1  14637  swrdccatin2  14664  pfxccatin12  14668  pfxccatpfx2  14672  pfxccat3a  14673  splfv2a  14691  splval2  14692  revcl  14696  revccat  14701  revrev  14702  cshwmodn  14730  cshwsublen  14731  cshwn  14732  cshwidxmod  14738  2cshwid  14749  3cshw  14753  cshweqdif2  14754  revco  14769  ccatco  14770  ccat2s1fvwALT  14890  ofccat  14904  zabscl  15248  absrdbnd  15277  iseraltlem3  15619  fsum0diaglem  15711  modfsummods  15728  binomlem  15764  binom1p  15766  incexc2  15773  climcndslem1  15784  geoser  15802  pwm1geoser  15804  geolim2  15806  mertenslem1  15819  mertenslem2  15820  mertens  15821  binomfallfaclem2  15975  binomrisefac  15977  fallfacval4  15978  bpolydiflem  15989  ruclem10  16176  sumodd  16327  divalglem9  16340  divalgmod  16345  bitsfzolem  16373  bitsfzo  16374  bitsmod  16375  bitsfi  16376  bitsinv1lem  16380  sadcaddlem  16396  sadadd3  16400  sadaddlem  16405  sadadd  16406  sadasslem  16409  sadass  16410  sadeq  16411  bitsres  16412  bitsuz  16413  bitsshft  16414  smuval2  16421  smupvallem  16422  smupval  16427  smueqlem  16429  smumullem  16431  smumul  16432  gcdcllem1  16438  zeqzmulgcd  16449  gcd0id  16458  gcdneg  16461  modgcd  16471  gcdmultipled  16473  bezoutlem4  16481  dvdsgcdb  16484  gcdass  16486  mulgcd  16487  gcdzeq  16491  dvdsmulgcd  16495  bezoutr  16507  bezoutr1  16508  nn0seqcvgd  16509  algfx  16519  eucalginv  16523  eucalg  16526  gcddvdslcm  16541  lcmneg  16542  lcmgcdlem  16545  lcmdvds  16547  lcmgcdeq  16551  lcmdvdsb  16552  lcmass  16553  lcmftp  16575  lcmfunsnlem1  16576  lcmfunsnlem2lem1  16577  lcmfunsnlem2lem2  16578  lcmfunsnlem2  16579  lcmfdvdsb  16582  lcmfun  16584  lcmfass  16585  mulgcddvds  16594  rpmulgcd2  16595  qredeu  16597  divgcdcoprm0  16604  sqnprm  16641  prmdvdsbc  16665  divnumden  16687  powm2modprm  16743  coprimeprodsq  16748  iserodd  16775  pclem  16778  pcpre1  16782  pcpremul  16783  pcqcl  16796  pcdvdsb  16809  pcidlem  16812  pc2dvds  16819  pcprmpw2  16822  dvdsprmpweqle  16826  pcadd  16829  pcfac  16839  pcbc  16840  pockthlem  16845  prmreclem2  16857  prmreclem3  16858  mul4sqlem  16893  4sqlem11  16895  4sqlem12  16896  4sqlem14  16898  vdwapun  16914  prmgaplcmlem1  16991  chnind  18556  chnub  18557  chnpolfz  18568  lagsubg  19136  psgnuni  19440  psgnran  19456  odmodnn0  19481  mndodconglem  19482  mndodcong  19483  odm1inv  19494  odmulg2  19496  odmulg  19497  odmulgeq  19498  odbezout  19499  odinv  19502  odf1  19503  gexod  19527  gexdvds3  19531  sylow1lem1  19539  sylow1lem3  19541  pgpfi  19546  pgpssslw  19555  sylow2alem2  19559  sylow2blem3  19563  fislw  19566  sylow3lem4  19571  sylow3lem6  19573  efginvrel2  19668  efgredlemf  19682  efgredlemd  19685  efgredlemc  19686  efgredlem  19688  efgcpbllemb  19696  odadd1  19789  odadd2  19790  gexexlem  19793  gexex  19794  torsubg  19795  lt6abl  19836  gsummulg  19883  ablfacrplem  20008  ablfacrp  20009  ablfacrp2  20010  ablfac1b  20013  ablfac1c  20014  ablfac1eulem  20015  ablfac1eu  20016  pgpfac1lem2  20018  pgpfaclem1  20024  ablfaclem3  20030  srgbinomlem3  20175  srgbinomlem4  20176  chrid  21492  znunit  21530  freshmansdream  21541  psgnghm  21547  asclmulg  21870  psrbaglefi  21894  psdvsca  22119  psdmul  22121  chfacfscmulfsupp  22815  chfacfpmmulfsupp  22819  cpmadugsumlemF  22832  dyadss  25563  dyaddisjlem  25564  ply1divex  26110  ply1termlem  26176  plyeq0lem  26183  plyaddlem1  26186  plymullem1  26187  coeeulem  26197  coeidlem  26210  coeeq2  26215  coemulhi  26227  dvply1  26259  dvply2g  26260  dvply2gOLD  26261  plydivex  26273  elqaalem2  26296  aareccl  26302  aannenlem1  26304  aalioulem1  26308  taylplem1  26338  taylplem2  26339  taylpfval  26340  dvtaylp  26346  taylthlem2  26350  taylthlem2OLD  26351  dvradcnv  26398  abelthlem7  26416  cxpeq  26735  birthdaylem2  26930  ftalem1  27051  basellem3  27061  isppw2  27093  isnsqf  27113  mule1  27126  ppinncl  27152  musum  27169  chtublem  27190  pclogsum  27194  vmasum  27195  dchrabs  27239  bcmax  27257  bposlem1  27263  bposlem6  27268  lgsval2lem  27286  lgsmod  27302  lgsne0  27314  gausslemma2dlem0h  27342  gausslemma2dlem0i  27343  gausslemma2dlem2  27346  gausslemma2dlem6  27351  gausslemma2d  27353  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem3  27356  lgseisenlem4  27357  lgsquadlem1  27359  m1lgs  27367  2lgslem1a  27370  2lgslem3a  27375  2lgslem3b  27376  2lgslem3c  27377  2lgslem3d  27378  2lgslem3d1  27382  2lgsoddprmlem2  27388  2sqlem8  27405  2sqcoprm  27414  2sqmod  27415  chebbnd1lem1  27448  dchrisumlem1  27468  dchrisum0flblem1  27487  selberg2lem  27529  ostth2lem2  27613  ostth2lem3  27614  finsumvtxdg2sstep  29635  finsumvtxdgeven  29638  vtxdgoddnumeven  29639  redwlklem  29755  wlkdlem1  29766  pthdlem1  29851  crctcshwlkn0lem4  29898  wwlksnredwwlkn0  29981  wwlksnextproplem2  29995  clwwlkccatlem  30076  clwlkclwwlkfo  30096  clwwlkwwlksb  30141  clwwlkndivn  30167  eupth2lem3lem3  30317  eupth2lem3lem4  30318  eupth2lem3  30323  eupth2lems  30325  numclwwlk5  30475  numclwwlk6  30477  ex-ind-dvds  30548  nndiffz1  32877  fzo0opth  32894  ccatf1  33042  pfxlsw2ccat  33043  wrdt2ind  33046  gsummulsubdishift1  33162  gsumwrd2dccatlem  33171  cycpmfv1  33207  cycpmco2lem2  33221  cycpmco2lem3  33222  cycpmco2lem4  33223  cycpmco2lem5  33224  cycpmco2lem6  33225  cycpmco2  33227  cycpmrn  33237  cyc3genpm  33246  cycpmconjslem2  33249  cyc3conja  33251  archirng  33282  archirngz  33283  archiabllem1a  33285  gsumind  33438  elrspunidl  33521  ply1coedeg  33682  ply1degltel  33687  gsummoncoe1fz  33691  esplyfval2  33742  esplympl  33744  esplyfval3  33749  esplyindfv  33753  vietalem  33756  ply1degltdimlem  33800  fldextrspundgdvds  33859  algextdeglem8  33902  rtelextdg2  33905  constrext2chnlem  33928  cos9thpiminplylem2  33961  cos9thpiminplylem3  33962  cos9thpiminplylem6  33965  cos9thpiminply  33966  madjusmdetlem4  34008  zrhcntr  34157  qqhval2lem  34159  oddpwdc  34532  eulerpartlems  34538  eulerpartlemb  34546  sseqfv1  34567  sseqfn  34568  sseqmw  34569  sseqf  34570  sseqfv2  34572  sseqp1  34573  ccatmulgnn0dir  34720  signsplypnf  34728  signsply0  34729  signslema  34740  signstfvn  34747  signstfvp  34749  signstfvc  34752  fsum2dsub  34785  reprinfz1  34800  reprfi2  34801  hashrepr  34803  reprdifc  34805  breprexplema  34808  breprexplemc  34810  circlemeth  34818  circlevma  34820  circlemethhgt  34821  hgt750lema  34835  tgoldbachgtde  34838  lpadlem3  34856  revpfxsfxrev  35332  revwlk  35341  subfacval3  35405  bcprod  35954  bccolsum  35955  fwddifnp1  36381  knoppndvlem6  36739  knoppndvlem7  36740  knoppndvlem10  36743  knoppndvlem14  36747  knoppndvlem15  36748  knoppndvlem16  36749  knoppndvlem17  36750  knoppndvlem19  36752  knoppndvlem21  36754  dfgcd3  37579  poimirlem3  37874  poimirlem4  37875  poimirlem6  37877  poimirlem13  37884  poimirlem14  37885  poimirlem17  37888  poimirlem21  37892  poimirlem22  37893  poimirlem23  37894  poimirlem26  37897  poimirlem27  37898  poimirlem31  37902  geomcau  38010  bccl2d  42361  lcmineqlem12  42410  lcmineqlem17  42415  dvrelogpow2b  42438  aks4d1p1p2  42440  aks4d1p1p4  42441  aks4d1p1p6  42443  aks4d1p1p7  42444  aks4d1p1p5  42445  aks4d1p1  42446  aks4d1p3  42448  aks4d1p6  42451  aks4d1p8d2  42455  aks4d1p8d3  42456  aks4d1p8  42457  primrootscoprmpow  42469  primrootlekpowne0  42475  aks6d1c1  42486  aks6d1c2p2  42489  aks6d1c2lem4  42497  aks6d1c2  42500  aks6d1c5lem3  42507  aks6d1c5lem2  42508  2np3bcnp1  42514  sticksstones5  42520  sticksstones6  42521  sticksstones7  42522  sticksstones10  42525  sticksstones11  42526  sticksstones12a  42527  sticksstones12  42528  sticksstones22  42538  aks6d1c6lem3  42542  bcled  42548  bcle2d  42549  aks6d1c7lem1  42550  aks6d1c7lem2  42551  grpods  42564  unitscyglem2  42566  unitscyglem4  42568  aks5lem8  42571  sumcubes  42683  gcdle1d  42700  gcdle2d  42701  frlmvscadiccat  42876  fltdiv  42994  flt4lem4  43007  fltnltalem  43020  eldioph2lem1  43117  pellexlem5  43190  congrep  43330  jm2.18  43345  jm2.19lem1  43346  jm2.19lem2  43347  jm2.19  43350  jm2.22  43352  jm2.23  43353  jm2.20nn  43354  jm2.25  43356  jm2.26a  43357  jm2.26lem3  43358  jm2.26  43359  jm2.27a  43362  jm2.27b  43363  jm2.27c  43364  jm3.1  43377  expdiophlem1  43378  hbtlem5  43485  radcnvrat  44670  nzin  44674  bccbc  44701  binomcxplemnn0  44705  binomcxplemnotnn0  44712  fprodexp  45954  mccllem  45957  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  dvnxpaek  46300  dvnmul  46301  dvnprodlem1  46304  dvnprodlem2  46305  wallispilem1  46423  wallispilem5  46427  stirlinglem3  46434  stirlinglem5  46436  stirlinglem7  46438  stirlinglem8  46439  fourierdlem102  46566  fourierdlem114  46578  sqwvfoura  46586  elaa2lem  46591  etransclem10  46602  etransclem20  46612  etransclem21  46613  etransclem22  46614  etransclem23  46615  etransclem24  46616  etransclem27  46619  etransclem28  46620  etransclem35  46627  etransclem38  46630  etransclem44  46636  etransclem45  46637  etransclem46  46638  sge0ad2en  46789  chnsubseqwl  47237  chnsubseq  47238  fsummmodsnunz  47735  fmtnoge3  47890  fmtnof1  47895  fmtnorec1  47897  sqrtpwpw2p  47898  fmtnodvds  47904  goldbachthlem2  47906  fmtnoprmfac2lem1  47926  lighneallem3  47967  lighneallem4b  47969  lighneallem4  47970  ssnn0ssfz  48709  altgsumbcALT  48713  flnn0ohalf  48894  dig2nn1st  48965  0dig2nn0o  48973  aacllem  50160