Theorem nnzd 11039

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 10925	. 2 |- ( ph -> A e. NN0 )
3	2	nn0zd 11038	1 |- ( ph -> A e. ZZ )

Syntax hints:   -> wi 4   e. wcel 1870   NNcn 10609   ZZcz 10937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615

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 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  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 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-er 7371  df-en 7578  df-dom 7579  df-sdom 7580  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-nn 10610  df-n0 10870  df-z 10938

This theorem is referenced by:  expaddzlem  12312  expmulz  12315  expmulnbnd  12401  facndiv  12470  bcval5  12500  bcpasc  12503  hashf1  12615  isercolllem1  13706  isercolllem2  13707  o1fsum  13851  bcxmas  13871  climcndslem2  13886  climcnds  13887  mertenslem1  13918  fprodser  13981  bpolydiflem  14085  eftlub  14141  eirrlem  14234  rpnnen2lem7  14251  rpnnen2lem9  14253  rpnnen2lem11  14255  sqr2irrlem  14278  dvdsfac  14338  dvdsmod  14340  bitsfzolem  14382  bitsmod  14384  bitsfi  14385  bitscmp  14386  bitsinv1  14390  sadadd3  14409  sadaddlem  14414  bitsuz  14422  bitsshft  14423  gcdnncl  14455  gcd1  14470  bezoutlem3  14479  bezoutlem4  14480  mulgcd  14485  gcdmultiplez  14490  rplpwr  14495  rppwr  14496  sqgcd  14497  dvdssq  14499  lcmneg  14539  lcmgcdlem  14542  prmz  14597  prmind2  14606  divgcdodd  14624  isprm6  14637  prmexpb  14641  prmfac1  14642  rpexp  14643  rpdvds  14647  coprmprod  14649  coprmproddvdslem  14650  numdensq  14674  hashdvds  14692  phiprmpw  14693  crt  14695  phimullem  14696  eulerthlem1  14698  eulerthlem2  14699  prmdivdiv  14704  odzdvds  14709  pythagtriplem4  14732  pythagtriplem6  14734  pythagtriplem7  14735  pythagtriplem11  14738  pythagtriplem13  14740  pythagtriplem19  14746  pclem  14751  pcprendvds2  14754  pcpre1  14755  pcpremul  14756  pceulem  14758  pcqmul  14766  pcdvdsb  14781  pcidlem  14784  pcdvdstr  14788  pcgcd1  14789  pc2dvds  14791  pcprmpw2  14794  pcaddlem  14796  pcadd  14797  pcmpt2  14801  pcmptdvds  14802  pcfac  14807  pcbc  14808  qexpz  14809  prmpwdvds  14811  pockthlem  14812  pockthg  14813  prmreclem2  14824  prmreclem3  14825  prmreclem4  14826  prmreclem5  14827  prmreclem6  14828  4sqlem5  14849  4sqlem8  14852  4sqlem9  14853  4sqlem10  14854  4sqlem12  14863  4sqlem14OLD  14865  4sqlem16OLD  14867  4sqlem17OLD  14868  4sqlem14  14871  4sqlem16  14873  4sqlem17  14874  vdwlem1  14894  vdwlem2  14895  vdwlem3  14896  vdwlem6  14899  vdwlem9  14902  vdwlem10  14903  vdwnnlem3  14910  prmdvdsprmop  14964  prmolelcmf  14969  prmgaplem1  14970  prmgaplcmlem1OLD  14975  prmdvdsprmorpOLD  14979  prmorlelcmfOLD  14983  prmorlelcmsOLDOLD  14985  prmgaplem7  14990  prmgaplem8  14991  gsumwsubmcl  16573  gsumccat  16576  gsumwmhm  16580  mulgneg  16727  mulgnndir  16731  psgnunilem4  17089  odlem2  17130  mndodconglem  17132  odmod  17137  gexlem2  17169  gexcl3  17174  gexcl2  17176  sylow1lem1  17185  sylow1lem3  17187  sylow1lem5  17189  pgpfi  17192  fislw  17212  sylow3lem4  17217  gexexlem  17425  ablfacrplem  17633  ablfacrp  17634  ablfacrp2  17635  ablfac1lem  17636  ablfac1b  17638  ablfac1eu  17641  pgpfac1lem3a  17644  ablfaclem3  17655  znrrg  19067  cayhamlem1  19821  caublcls  22171  ovolicc2lem4  22351  iundisj2  22379  volsup  22386  uniioombllem3  22420  mbfi1fseqlem3  22552  mbfi1fseqlem4  22553  elqaalem2  23141  aalioulem1  23153  aalioulem4  23156  aalioulem5  23157  aalioulem6  23158  aaliou  23159  aaliou3lem1  23163  aaliou3lem2  23164  aaliou3lem3  23165  aaliou3lem8  23166  aaliou3lem5  23168  aaliou3lem6  23169  aaliou3lem7  23170  taylthlem2  23194  cxpeq  23562  amgmlem  23780  lgamgulmlem4  23822  lgamcvg2  23845  wilthlem2  23859  wilth  23861  ftalem5  23866  basellem2  23871  basellem3  23872  basellem4  23873  basellem5  23874  muval1  23923  dvdssqf  23928  sgmnncl  23937  efchtdvds  23949  mumullem2  23970  mumul  23971  sqff1o  23972  fsumdvdsdiaglem  23975  dvdsppwf1o  23978  dvdsflf1o  23979  muinv  23985  dvdsmulf1o  23986  chtublem  24002  fsumvma2  24005  vmasum  24007  chpchtsum  24010  logfacubnd  24012  mersenne  24018  perfect1  24019  perfectlem1  24020  perfectlem2  24021  perfect  24022  dchrelbas4  24034  dchrfi  24046  bcmono  24068  bcp1ctr  24070  bclbnd  24071  bposlem1  24075  bposlem3  24077  bposlem5  24079  bposlem6  24080  bposlem9  24083  lgsmod  24112  lgsdir  24121  lgsdilem2  24122  lgsne0  24124  lgsqrlem2  24133  lgsqr  24137  lgseisenlem1  24140  lgseisenlem2  24141  lgseisenlem3  24142  lgseisenlem4  24143  lgsquadlem1  24145  lgsquadlem2  24146  lgsquadlem3  24147  lgsquad2lem1  24149  lgsquad2lem2  24150  lgsquad2  24151  m1lgs  24153  2sqlem3  24157  2sqlem4  24158  2sqlem8  24163  chebbnd1lem1  24170  rplogsumlem2  24186  rpvmasumlem  24188  dchrisumlem1  24190  dchrisumlem2  24191  dchrisumlem3  24192  dchrisum0fmul  24207  dchrisum0ff  24208  dchrisum0flblem1  24209  dchrisum0flblem2  24210  dchrisum0flb  24211  dchrisum0  24221  pntrsumbnd2  24268  pntrlog2bndlem1  24278  pntrlog2bndlem6  24284  pntpbnd2  24288  pntlemg  24299  pntlemj  24304  pntlemf  24306  ostth2lem2  24335  ostth2lem3  24336  ostth3  24339  minvecolem4  26367  iundisj2f  28039  ssnnssfz  28203  iundisj2fi  28209  f1ocnt  28212  numdenneg  28218  ltesubnnd  28223  isarchi3  28342  archiabllem1b  28347  psgnfzto1stlem  28452  smatrcl  28461  1smat1  28469  submateqlem1  28472  submateqlem2  28473  lmatfvlem  28480  qqhval2  28625  qqhf  28629  qqhghm  28631  qqhrhm  28632  qqhnm  28633  qqhre  28663  esumcvg  28746  meascnbl  28880  omssubadd  28961  oddpwdc  29013  ballotlemfp1  29150  ballotlemfc0  29151  ballotlemfcc  29152  ballotlemimin  29164  ballotlemic  29165  ballotlem1c  29166  subfaclim  29699  cvmliftlem7  29802  sinccvglem  30104  bcprod  30161  bccolsum  30162  faclimlem2  30167  faclim2  30171  poimirlem1  31645  poimirlem2  31646  poimirlem3  31647  poimirlem4  31648  poimirlem6  31650  poimirlem8  31652  poimirlem9  31653  poimirlem10  31654  poimirlem11  31655  poimirlem13  31657  poimirlem14  31658  poimirlem15  31659  poimirlem16  31660  poimirlem17  31661  poimirlem18  31662  poimirlem19  31663  poimirlem20  31664  poimirlem21  31665  poimirlem22  31666  poimirlem23  31667  poimirlem24  31668  poimirlem26  31670  poimirlem27  31671  poimirlem28  31672  poimirlem31  31675  mblfinlem2  31682  seqpo  31780  incsequz  31781  incsequz2  31782  irrapxlem3  35378  irrapxlem5  35380  pellexlem5  35387  pellexlem6  35388  pellex  35389  pell1234qrmulcl  35409  jm2.23  35557  jm2.20nn  35558  jm2.26lem3  35562  jm2.27a  35566  jm2.27b  35567  jm2.27c  35568  jm3.1lem1  35578  jm3.1lem3  35580  hashgcdlem  35773  inductionexd  36230  nznngen  36302  hashnzfz2  36307  fmuldfeq  37233  divcnvg  37279  stoweidlem1  37430  stoweidlem3  37432  stoweidlem11  37440  stoweidlem20  37449  stoweidlem26  37455  stoweidlem34  37464  stoweidlem51  37481  stirlinglem4  37508  stirlinglem5  37509  stirlinglem8  37512  dirkerper  37527  dirkertrigeqlem2  37530  dirkertrigeqlem3  37531  dirkercncflem2  37535  fourierdlem11  37549  fourierdlem14  37552  fourierdlem20  37558  fourierdlem25  37563  fourierdlem37  37575  fourierdlem41  37579  fourierdlem48  37586  fourierdlem49  37587  fourierdlem54  37592  fourierdlem64  37602  fourierdlem73  37611  fourierdlem79  37617  fourierdlem92  37630  fourierdlem93  37631  fourierdlem111  37649  sqwvfourb  37661  etransclem3  37669  etransclem7  37673  etransclem10  37676  etransclem15  37681  etransclem24  37690  etransclem25  37691  etransclem26  37692  etransclem27  37693  etransclem28  37694  etransclem35  37701  etransclem37  37703  etransclem38  37704  etransclem41  37707  etransclem44  37710  etransclem45  37711  etransclem48  37714  iccpartgtprec  38124  iccpartipre  38125  divgcdoddALTV  38201  perfectALTVlem1  38233  perfectALTVlem2  38234  perfectALTV  38235  gboge7  38254  proththdlem  38303  proththd  38304  pw2m1lepw2m1  39079  nnolog2flm1  39162  dignn0fr  39173  dignn0flhalflem1  39187