Theorem nnzd 11047

Description: A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
nnzd.1	|- ( ph -> A e. NN )

Assertion

Ref	Expression
nnzd	|- ( ph -> A e. ZZ )

Proof of Theorem nnzd

Step	Hyp	Ref	Expression
1		nnzd.1	. . 3 |- ( ph -> A e. NN )
2	1	nnnn0d 10933	. 2 |- ( ph -> A e. NN0 )
3	2	nn0zd 11046	1 |- ( ph -> A e. ZZ )

Syntax hints:   -> wi 4   e. wcel 1872   NNcn 10617   ZZcz 10945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598  ax-resscn 9604  ax-1cn 9605  ax-icn 9606  ax-addcl 9607  ax-addrcl 9608  ax-mulcl 9609  ax-mulrcl 9610  ax-mulcom 9611  ax-addass 9612  ax-mulass 9613  ax-distr 9614  ax-i2m1 9615  ax-1ne0 9616  ax-1rid 9617  ax-rnegex 9618  ax-rrecex 9619  ax-cnre 9620  ax-pre-lttri 9621  ax-pre-lttrn 9622  ax-pre-ltadd 9623  ax-pre-mulgt0 9624

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6268  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-om 6708  df-wrecs 7040  df-recs 7102  df-rdg 7140  df-er 7375  df-en 7582  df-dom 7583  df-sdom 7584  df-pnf 9685  df-mnf 9686  df-xr 9687  df-ltxr 9688  df-le 9689  df-sub 9870  df-neg 9871  df-nn 10618  df-n0 10878  df-z 10946

This theorem is referenced by:  expaddzlem  12322  expmulz  12325  expmulnbnd  12411  facndiv  12480  bcval5  12510  bcpasc  12513  hashf1  12625  isercolllem1  13728  isercolllem2  13729  o1fsum  13873  bcxmas  13893  climcndslem2  13908  climcnds  13909  mertenslem1  13940  fprodser  14003  bpolydiflem  14107  eftlub  14163  eirrlem  14256  rpnnen2lem7  14273  rpnnen2lem9  14275  rpnnen2lem11  14277  sqr2irrlem  14300  dvdsfac  14360  dvdsmod  14362  bitsfzolem  14407  bitsfzolemOLD  14408  bitsmod  14410  bitsfi  14411  bitscmp  14412  bitsinv1  14416  sadadd3  14435  sadaddlem  14440  bitsuz  14448  bitsshft  14449  gcdnncl  14481  gcd1  14496  bezoutlem3OLD  14505  bezoutlem4OLD  14506  bezoutlem3  14508  bezoutlem4  14509  mulgcd  14514  gcdmultiplez  14519  rplpwr  14524  rppwr  14525  sqgcd  14526  dvdssq  14528  lcmneg  14568  lcmgcdlem  14571  prmz  14626  prmind2  14635  divgcdodd  14653  isprm6  14666  prmexpb  14670  prmfac1  14671  rpexp  14672  rpdvds  14676  coprmprod  14678  coprmproddvdslem  14679  numdensq  14703  hashdvds  14723  phiprmpw  14724  crt  14726  phimullem  14727  eulerthlem1  14729  eulerthlem2  14730  prmdivdiv  14735  odzdvds  14740  odzdvdsOLD  14746  pythagtriplem4  14769  pythagtriplem6  14771  pythagtriplem7  14772  pythagtriplem11  14775  pythagtriplem13  14777  pythagtriplem19  14783  pclem  14788  pcprendvds2  14791  pcpre1  14792  pcpremul  14793  pceulem  14795  pcqmul  14803  pcdvdsb  14818  pcidlem  14821  pcdvdstr  14825  pcgcd1  14826  pc2dvds  14828  pcprmpw2  14831  pcaddlem  14833  pcadd  14834  pcmpt2  14838  pcmptdvds  14839  pcfac  14844  pcbc  14845  qexpz  14846  prmpwdvds  14848  pockthlem  14849  pockthg  14850  prmreclem2  14861  prmreclem3  14862  prmreclem4  14863  prmreclem5  14864  prmreclem6  14865  4sqlem5  14886  4sqlem8  14889  4sqlem9  14890  4sqlem10  14891  4sqlem12  14900  4sqlem14OLD  14902  4sqlem16OLD  14904  4sqlem17OLD  14905  4sqlem14  14908  4sqlem16  14910  4sqlem17  14911  vdwlem1  14931  vdwlem2  14932  vdwlem3  14933  vdwlem6  14936  vdwlem9  14939  vdwlem10  14940  vdwnnlem3  14947  prmdvdsprmop  15001  prmolelcmf  15006  prmgaplem1  15007  prmgaplcmlem1OLD  15012  prmdvdsprmorpOLD  15016  prmorlelcmfOLD  15020  prmorlelcmsOLDOLD  15022  prmgaplem7  15027  prmgaplem8  15028  gsumwsubmcl  16622  gsumccat  16625  gsumwmhm  16629  mulgneg  16776  mulgnndir  16780  psgnunilem4  17138  odlem2  17188  mndodconglem  17190  odmod  17195  odlem2OLD  17204  gexlem2  17233  gexlem2OLD  17236  gexcl3  17239  gexcl2  17241  sylow1lem1  17250  sylow1lem3  17252  sylow1lem5  17254  pgpfi  17257  fislw  17277  sylow3lem4  17282  gexexlem  17490  ablfacrplem  17698  ablfacrp  17699  ablfacrp2  17700  ablfac1lem  17701  ablfac1b  17703  ablfac1eu  17706  pgpfac1lem3a  17709  ablfaclem3  17720  znrrg  19135  cayhamlem1  19889  caublcls  22277  ovolicc2lem4OLD  22472  ovolicc2lem4  22473  iundisj2  22501  volsup  22508  uniioombllem3  22542  mbfi1fseqlem3  22674  mbfi1fseqlem4  22675  elqaalem2  23272  elqaalem2OLD  23275  aalioulem1  23287  aalioulem4  23290  aalioulem5  23291  aalioulem6  23292  aaliou  23293  aaliou3lem1  23297  aaliou3lem2  23298  aaliou3lem3  23299  aaliou3lem8  23300  aaliou3lem5  23302  aaliou3lem6  23303  aaliou3lem7  23304  taylthlem2  23328  cxpeq  23696  amgmlem  23914  lgamgulmlem4  23956  lgamcvg2  23979  wilthlem2  23993  wilth  23995  ftalem5  24000  ftalem5OLD  24002  basellem2  24007  basellem3  24008  basellem4  24009  basellem5  24010  muval1  24059  dvdssqf  24064  sgmnncl  24073  efchtdvds  24085  mumullem2  24106  mumul  24107  sqff1o  24108  fsumdvdsdiaglem  24111  dvdsppwf1o  24114  dvdsflf1o  24115  muinv  24121  dvdsmulf1o  24122  chtublem  24138  fsumvma2  24141  vmasum  24143  chpchtsum  24146  logfacubnd  24148  mersenne  24154  perfect1  24155  perfectlem1  24156  perfectlem2  24157  perfect  24158  dchrelbas4  24170  dchrfi  24182  bcmono  24204  bcp1ctr  24206  bclbnd  24207  bposlem1  24211  bposlem3  24213  bposlem5  24215  bposlem6  24216  bposlem9  24219  lgsmod  24248  lgsdir  24257  lgsdilem2  24258  lgsne0  24260  lgsqrlem2  24269  lgsqr  24273  lgseisenlem1  24276  lgseisenlem2  24277  lgseisenlem3  24278  lgseisenlem4  24279  lgsquadlem1  24281  lgsquadlem2  24282  lgsquadlem3  24283  lgsquad2lem1  24285  lgsquad2lem2  24286  lgsquad2  24287  m1lgs  24289  2sqlem3  24293  2sqlem4  24294  2sqlem8  24299  chebbnd1lem1  24306  rplogsumlem2  24322  rpvmasumlem  24324  dchrisumlem1  24326  dchrisumlem2  24327  dchrisumlem3  24328  dchrisum0fmul  24343  dchrisum0ff  24344  dchrisum0flblem1  24345  dchrisum0flblem2  24346  dchrisum0flb  24347  dchrisum0  24357  pntrsumbnd2  24404  pntrlog2bndlem1  24414  pntrlog2bndlem6  24420  pntpbnd2  24424  pntlemg  24435  pntlemj  24440  pntlemf  24442  ostth2lem2  24471  ostth2lem3  24472  ostth3  24475  minvecolem4  26521  minvecolem4OLD  26531  iundisj2f  28203  ssnnssfz  28374  iundisj2fi  28380  f1ocnt  28383  numdenneg  28388  ltesubnnd  28393  isarchi3  28512  archiabllem1b  28517  psgnfzto1stlem  28622  smatrcl  28631  1smat1  28639  submateqlem1  28642  submateqlem2  28643  lmatfvlem  28650  qqhval2  28795  qqhf  28799  qqhghm  28801  qqhrhm  28802  qqhnm  28803  qqhre  28833  esumcvg  28916  meascnbl  29050  omssubadd  29137  omssubaddOLD  29141  oddpwdc  29196  ballotlemfp1  29333  ballotlemfc0  29334  ballotlemfcc  29335  ballotlemimin  29347  ballotlemic  29348  ballotlem1c  29349  ballotlemiminOLD  29385  ballotlemicOLD  29386  ballotlem1cOLD  29387  subfaclim  29920  cvmliftlem7  30023  sinccvglem  30325  bcprod  30382  bccolsum  30383  faclimlem2  30388  faclim2  30392  poimirlem1  31906  poimirlem2  31907  poimirlem3  31908  poimirlem4  31909  poimirlem6  31911  poimirlem8  31913  poimirlem9  31914  poimirlem10  31915  poimirlem11  31916  poimirlem13  31918  poimirlem14  31919  poimirlem15  31920  poimirlem16  31921  poimirlem17  31922  poimirlem18  31923  poimirlem19  31924  poimirlem20  31925  poimirlem21  31926  poimirlem22  31927  poimirlem23  31928  poimirlem24  31929  poimirlem26  31931  poimirlem27  31932  poimirlem28  31933  poimirlem31  31936  mblfinlem2  31943  seqpo  32041  incsequz  32042  incsequz2  32043  irrapxlem3  35639  irrapxlem5  35641  pellexlem5  35648  pellexlem6  35649  pellex  35650  pell1234qrmulcl  35672  jm2.23  35822  jm2.20nn  35823  jm2.26lem3  35827  jm2.27a  35831  jm2.27b  35832  jm2.27c  35833  jm3.1lem1  35843  jm3.1lem3  35845  hashgcdlem  36045  inductionexd  36564  nznngen  36636  hashnzfz2  36641  fmuldfeq  37602  divcnvg  37648  stoweidlem1  37802  stoweidlem3  37804  stoweidlem11  37812  stoweidlem20  37821  stoweidlem26  37827  stoweidlem34  37836  stoweidlem51  37853  stirlinglem4  37880  stirlinglem5  37881  stirlinglem8  37884  dirkerper  37899  dirkertrigeqlem2  37902  dirkertrigeqlem3  37903  dirkercncflem2  37907  fourierdlem11  37921  fourierdlem14  37924  fourierdlem20  37930  fourierdlem25  37935  fourierdlem37  37948  fourierdlem41  37952  fourierdlem48  37959  fourierdlem49  37960  fourierdlem54  37965  fourierdlem64  37975  fourierdlem73  37984  fourierdlem79  37990  fourierdlem92  38003  fourierdlem93  38004  fourierdlem111  38022  sqwvfourb  38034  etransclem3  38043  etransclem7  38047  etransclem10  38050  etransclem15  38055  etransclem24  38064  etransclem25  38065  etransclem26  38066  etransclem27  38067  etransclem28  38068  etransclem35  38075  etransclem37  38077  etransclem38  38078  etransclem41  38081  etransclem44  38084  etransclem45  38085  etransclem48OLD  38088  etransclem48  38089  ovnsubaddlem1  38297  iccpartgtprec  38605  iccpartipre  38606  divgcdoddALTV  38682  perfectALTVlem1  38714  perfectALTVlem2  38715  perfectALTV  38716  gboge7  38735  proththdlem  38784  proththd  38785  pw2m1lepw2m1  39969  nnolog2flm1  40052  dignn0fr  40063  dignn0flhalflem1  40077