Theorem nnzd 10330

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

Syntax hints:   -> wi 4   e. wcel 1721   NNcn 9956   ZZcz 10238

This theorem is referenced by:  expaddzlem  11378  expmulz  11381  expmulnbnd  11466  facndiv  11534  bcval5  11564  bcpasc  11567  hashf1  11661  isercolllem1  12413  isercolllem2  12414  o1fsum  12547  bcxmas  12570  climcndslem2  12585  climcnds  12586  mertenslem1  12616  eftlub  12665  eirrlem  12758  rpnnen2lem7  12775  rpnnen2lem9  12777  rpnnen2lem11  12779  sqr2irrlem  12802  dvdsfac  12859  dvdsmod  12861  bitsfzolem  12901  bitsmod  12903  bitsfi  12904  bitscmp  12905  bitsinv1  12909  sadadd3  12928  sadaddlem  12933  bitsuz  12941  bitsshft  12942  gcd1  12987  bezoutlem3  12995  bezoutlem4  12996  mulgcd  13001  gcdmultiplez  13006  rplpwr  13011  rppwr  13012  sqgcd  13013  dvdssq  13015  prmz  13038  prmind2  13045  isprm6  13064  prmexpb  13072  prmfac1  13073  divgcdodd  13074  rpexp  13075  rpdvds  13079  numdensq  13101  hashdvds  13119  phiprmpw  13120  crt  13122  phimullem  13123  eulerthlem1  13125  eulerthlem2  13126  prmdivdiv  13131  odzdvds  13136  pythagtriplem4  13148  pythagtriplem6  13150  pythagtriplem7  13151  pythagtriplem11  13154  pythagtriplem13  13156  pythagtriplem19  13162  pclem  13167  pcprendvds2  13170  pcpre1  13171  pcpremul  13172  pceulem  13174  pcqmul  13182  pcdvdsb  13197  pcidlem  13200  pcdvdstr  13204  pcgcd1  13205  pc2dvds  13207  pcprmpw2  13210  pcaddlem  13212  pcadd  13213  pcmpt2  13217  pcmptdvds  13218  pcfac  13223  pcbc  13224  qexpz  13225  prmpwdvds  13227  pockthlem  13228  pockthg  13229  prmreclem2  13240  prmreclem3  13241  prmreclem4  13242  prmreclem5  13243  prmreclem6  13244  4sqlem5  13265  4sqlem8  13268  4sqlem9  13269  4sqlem10  13270  4sqlem12  13279  4sqlem14  13281  4sqlem16  13283  4sqlem17  13284  vdwlem1  13304  vdwlem2  13305  vdwlem3  13306  vdwlem6  13309  vdwlem9  13312  vdwlem10  13313  vdwnnlem3  13320  gsumwsubmcl  14739  gsumccat  14742  gsumwmhm  14745  mulgneg  14863  mulgnndir  14867  odlem2  15132  mndodconglem  15134  odmod  15139  gexlem2  15171  gexcl3  15176  gexcl2  15178  sylow1lem1  15187  sylow1lem3  15189  sylow1lem5  15191  pgpfi  15194  fislw  15214  sylow3lem4  15219  gexexlem  15422  ablfacrplem  15578  ablfacrp  15579  ablfacrp2  15580  ablfac1lem  15581  ablfac1b  15583  ablfac1eu  15586  pgpfac1lem3a  15589  ablfaclem3  15600  caublcls  19214  ovolicc2lem4  19369  iundisj2  19396  volsup  19403  uniioombllem3  19430  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  elqaalem2  20190  aalioulem1  20202  aalioulem4  20205  aalioulem5  20206  aalioulem6  20207  aaliou  20208  aaliou3lem1  20212  aaliou3lem2  20213  aaliou3lem3  20214  aaliou3lem8  20215  aaliou3lem5  20217  aaliou3lem6  20218  aaliou3lem7  20219  taylthlem2  20243  cxpeq  20594  amgmlem  20781  wilthlem2  20805  wilth  20807  ftalem5  20812  basellem2  20817  basellem3  20818  basellem4  20819  basellem5  20820  muval1  20869  dvdssqf  20874  sgmnncl  20883  efchtdvds  20895  mumullem2  20916  mumul  20917  sqff1o  20918  fsumdvdsdiaglem  20921  dvdsppwf1o  20924  dvdsflf1o  20925  muinv  20931  dvdsmulf1o  20932  chtublem  20948  fsumvma2  20951  vmasum  20953  chpchtsum  20956  logfacubnd  20958  mersenne  20964  perfect1  20965  perfectlem1  20966  perfectlem2  20967  perfect  20968  dchrelbas4  20980  dchrfi  20992  bcmono  21014  bcp1ctr  21016  bclbnd  21017  bposlem1  21021  bposlem3  21023  bposlem5  21025  bposlem6  21026  bposlem9  21029  lgsmod  21058  lgsdir  21067  lgsdilem2  21068  lgsne0  21070  lgsqrlem2  21079  lgsqr  21083  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem3  21088  lgseisenlem4  21089  lgsquadlem1  21091  lgsquadlem2  21092  lgsquadlem3  21093  lgsquad2lem1  21095  lgsquad2lem2  21096  lgsquad2  21097  m1lgs  21099  2sqlem3  21103  2sqlem4  21104  2sqlem8  21109  chebbnd1lem1  21116  rplogsumlem2  21132  rpvmasumlem  21134  dchrisumlem1  21136  dchrisumlem2  21137  dchrisumlem3  21138  dchrisum0fmul  21153  dchrisum0ff  21154  dchrisum0flblem1  21155  dchrisum0flblem2  21156  dchrisum0flb  21157  dchrisum0  21167  pntrsumbnd2  21214  pntrlog2bndlem1  21224  pntrlog2bndlem6  21230  pntpbnd2  21234  pntlemg  21245  pntlemj  21250  pntlemf  21252  ostth2lem2  21281  ostth2lem3  21282  ostth3  21285  minvecolem4  22335  iundisj2f  23983  ssnnssfz  24101  iundisj2fi  24106  numdenneg  24113  ltesubnnd  24115  isarchi2  24208  qqhval2  24319  qqhf  24323  qqhghm  24325  qqhrhm  24326  qqhnm  24327  qqhre  24339  esumcvg  24429  meascnbl  24526  ballotlemfp1  24702  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemimin  24716  ballotlemic  24717  ballotlem1c  24718  lgamgulmlem4  24769  lgamcvg2  24792  subfaclim  24827  cvmliftlem7  24931  sinccvglem  25062  fprodser  25228  faclimlem2  25311  faclim2  25315  bpolydiflem  26004  mblfinlem  26143  seqpo  26341  incsequz  26342  incsequz2  26343  irrapxlem3  26777  irrapxlem5  26779  pellexlem5  26786  pellexlem6  26787  pellex  26788  pell1234qrmulcl  26808  jm2.23  26957  jm2.20nn  26958  jm2.26lem3  26962  jm2.27a  26966  jm2.27b  26967  jm2.27c  26968  jm3.1lem1  26978  jm3.1lem3  26980  psgnunilem4  27288  hashgcdlem  27384  fmuldfeq  27580  stoweidlem1  27617  stoweidlem3  27619  stoweidlem11  27627  stoweidlem20  27636  stoweidlem26  27642  stoweidlem34  27650  stoweidlem51  27667  stirlinglem4  27693  stirlinglem5  27694  stirlinglem8  27697

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-riota 6508  df-recs 6592  df-rdg 6627  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-nn 9957  df-n0 10178  df-z 10239