Theorem nnzd 11073

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

Syntax hints:   -> wi 4   e. wcel 1898   NNcn 10642   ZZcz 10971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-er 7394  df-en 7601  df-dom 7602  df-sdom 7603  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-nn 10643  df-n0 10904  df-z 10972

This theorem is referenced by:  expaddzlem  12353  expmulz  12356  expmulnbnd  12442  facndiv  12511  bcval5  12541  bcpasc  12544  hashf1  12659  isercolllem1  13783  isercolllem2  13784  o1fsum  13928  bcxmas  13948  climcndslem2  13963  climcnds  13964  mertenslem1  13995  fprodser  14058  bpolydiflem  14162  eftlub  14218  eirrlem  14311  rpnnen2lem7  14328  rpnnen2lem9  14330  rpnnen2lem11  14332  sqr2irrlem  14355  dvdsfac  14415  dvdsmod  14417  bitsfzolem  14462  bitsfzolemOLD  14463  bitsmod  14465  bitsfi  14466  bitscmp  14467  bitsinv1  14471  sadadd3  14490  sadaddlem  14495  bitsuz  14503  bitsshft  14504  gcdnncl  14536  gcd1  14551  bezoutlem3OLD  14560  bezoutlem4OLD  14561  bezoutlem3  14563  bezoutlem4  14564  mulgcd  14569  gcdmultiplez  14574  rplpwr  14579  rppwr  14580  sqgcd  14581  dvdssq  14583  lcmneg  14623  lcmgcdlem  14626  prmz  14681  prmind2  14690  divgcdodd  14708  isprm6  14721  prmexpb  14725  prmfac1  14726  rpexp  14727  rpdvds  14731  coprmprod  14733  coprmproddvdslem  14734  numdensq  14758  hashdvds  14778  phiprmpw  14779  crt  14781  phimullem  14782  eulerthlem1  14784  eulerthlem2  14785  prmdivdiv  14790  odzdvds  14795  odzdvdsOLD  14801  pythagtriplem4  14824  pythagtriplem6  14826  pythagtriplem7  14827  pythagtriplem11  14830  pythagtriplem13  14832  pythagtriplem19  14838  pclem  14843  pcprendvds2  14846  pcpre1  14847  pcpremul  14848  pceulem  14850  pcqmul  14858  pcdvdsb  14873  pcidlem  14876  pcdvdstr  14880  pcgcd1  14881  pc2dvds  14883  pcprmpw2  14886  pcaddlem  14888  pcadd  14889  pcmpt2  14893  pcmptdvds  14894  pcfac  14899  pcbc  14900  qexpz  14901  prmpwdvds  14903  pockthlem  14904  pockthg  14905  prmreclem2  14916  prmreclem3  14917  prmreclem4  14918  prmreclem5  14919  prmreclem6  14920  4sqlem5  14941  4sqlem8  14944  4sqlem9  14945  4sqlem10  14946  4sqlem12  14955  4sqlem14OLD  14957  4sqlem16OLD  14959  4sqlem17OLD  14960  4sqlem14  14963  4sqlem16  14965  4sqlem17  14966  vdwlem1  14986  vdwlem2  14987  vdwlem3  14988  vdwlem6  14991  vdwlem9  14994  vdwlem10  14995  vdwnnlem3  15002  prmdvdsprmop  15056  prmolelcmf  15061  prmgaplem1  15062  prmgaplcmlem1OLD  15067  prmdvdsprmorpOLD  15071  prmorlelcmfOLD  15075  prmorlelcmsOLDOLD  15077  prmgaplem7  15082  prmgaplem8  15083  gsumwsubmcl  16677  gsumccat  16680  gsumwmhm  16684  mulgneg  16831  mulgnndir  16835  psgnunilem4  17193  odlem2  17243  mndodconglem  17245  odmod  17250  odlem2OLD  17259  gexlem2  17288  gexlem2OLD  17291  gexcl3  17294  gexcl2  17296  sylow1lem1  17305  sylow1lem3  17307  sylow1lem5  17309  pgpfi  17312  fislw  17332  sylow3lem4  17337  gexexlem  17545  ablfacrplem  17753  ablfacrp  17754  ablfacrp2  17755  ablfac1lem  17756  ablfac1b  17758  ablfac1eu  17761  pgpfac1lem3a  17764  ablfaclem3  17775  znrrg  19191  cayhamlem1  19945  caublcls  22333  ovolicc2lem4OLD  22528  ovolicc2lem4  22529  iundisj2  22558  volsup  22565  uniioombllem3  22599  mbfi1fseqlem3  22731  mbfi1fseqlem4  22732  elqaalem2  23329  elqaalem2OLD  23332  aalioulem1  23344  aalioulem4  23347  aalioulem5  23348  aalioulem6  23349  aaliou  23350  aaliou3lem1  23354  aaliou3lem2  23355  aaliou3lem3  23356  aaliou3lem8  23357  aaliou3lem5  23359  aaliou3lem6  23360  aaliou3lem7  23361  taylthlem2  23385  cxpeq  23753  amgmlem  23971  lgamgulmlem4  24013  lgamcvg2  24036  wilthlem2  24050  wilth  24052  ftalem5  24057  ftalem5OLD  24059  basellem2  24064  basellem3  24065  basellem4  24066  basellem5  24067  muval1  24116  dvdssqf  24121  sgmnncl  24130  efchtdvds  24142  mumullem2  24163  mumul  24164  sqff1o  24165  fsumdvdsdiaglem  24168  dvdsppwf1o  24171  dvdsflf1o  24172  muinv  24178  dvdsmulf1o  24179  chtublem  24195  fsumvma2  24198  vmasum  24200  chpchtsum  24203  logfacubnd  24205  mersenne  24211  perfect1  24212  perfectlem1  24213  perfectlem2  24214  perfect  24215  dchrelbas4  24227  dchrfi  24239  bcmono  24261  bcp1ctr  24263  bclbnd  24264  bposlem1  24268  bposlem3  24270  bposlem5  24272  bposlem6  24273  bposlem9  24276  lgsmod  24305  lgsdir  24314  lgsdilem2  24315  lgsne0  24317  lgsqrlem2  24326  lgsqr  24330  lgseisenlem1  24333  lgseisenlem2  24334  lgseisenlem3  24335  lgseisenlem4  24336  lgsquadlem1  24338  lgsquadlem2  24339  lgsquadlem3  24340  lgsquad2lem1  24342  lgsquad2lem2  24343  lgsquad2  24344  m1lgs  24346  2sqlem3  24350  2sqlem4  24351  2sqlem8  24356  chebbnd1lem1  24363  rplogsumlem2  24379  rpvmasumlem  24381  dchrisumlem1  24383  dchrisumlem2  24384  dchrisumlem3  24385  dchrisum0fmul  24400  dchrisum0ff  24401  dchrisum0flblem1  24402  dchrisum0flblem2  24403  dchrisum0flb  24404  dchrisum0  24414  pntrsumbnd2  24461  pntrlog2bndlem1  24471  pntrlog2bndlem6  24477  pntpbnd2  24481  pntlemg  24492  pntlemj  24497  pntlemf  24499  ostth2lem2  24528  ostth2lem3  24529  ostth3  24532  minvecolem4  26578  minvecolem4OLD  26588  iundisj2f  28254  ssnnssfz  28419  iundisj2fi  28425  f1ocnt  28428  numdenneg  28432  ltesubnnd  28437  isarchi3  28555  archiabllem1b  28560  psgnfzto1stlem  28664  smatrcl  28673  1smat1  28681  submateqlem1  28684  submateqlem2  28685  lmatfvlem  28692  qqhval2  28837  qqhf  28841  qqhghm  28843  qqhrhm  28844  qqhnm  28845  qqhre  28875  esumcvg  28958  meascnbl  29092  omssubadd  29178  omssubaddOLD  29182  oddpwdc  29237  ballotlemfp1  29374  ballotlemfc0  29375  ballotlemfcc  29376  ballotlemimin  29388  ballotlemic  29389  ballotlem1c  29390  ballotlemiminOLD  29426  ballotlemicOLD  29427  ballotlem1cOLD  29428  subfaclim  29961  cvmliftlem7  30064  sinccvglem  30366  bcprod  30424  bccolsum  30425  faclimlem2  30430  faclim2  30434  poimirlem1  31987  poimirlem2  31988  poimirlem3  31989  poimirlem4  31990  poimirlem6  31992  poimirlem8  31994  poimirlem9  31995  poimirlem10  31996  poimirlem11  31997  poimirlem13  31999  poimirlem14  32000  poimirlem15  32001  poimirlem16  32002  poimirlem17  32003  poimirlem18  32004  poimirlem19  32005  poimirlem20  32006  poimirlem21  32007  poimirlem22  32008  poimirlem23  32009  poimirlem24  32010  poimirlem26  32012  poimirlem27  32013  poimirlem28  32014  poimirlem31  32017  mblfinlem2  32024  seqpo  32122  incsequz  32123  incsequz2  32124  irrapxlem3  35714  irrapxlem5  35716  pellexlem5  35723  pellexlem6  35724  pellex  35725  pell1234qrmulcl  35747  jm2.23  35897  jm2.20nn  35898  jm2.26lem3  35902  jm2.27a  35906  jm2.27b  35907  jm2.27c  35908  jm3.1lem1  35918  jm3.1lem3  35920  hashgcdlem  36120  inductionexd  36639  nznngen  36710  hashnzfz2  36715  fmuldfeq  37747  divcnvg  37793  stoweidlem1  37962  stoweidlem3  37964  stoweidlem11  37972  stoweidlem20  37981  stoweidlem26  37987  stoweidlem34  37996  stoweidlem51  38013  stirlinglem4  38040  stirlinglem5  38041  stirlinglem8  38044  dirkerper  38059  dirkertrigeqlem2  38062  dirkertrigeqlem3  38063  dirkercncflem2  38067  fourierdlem11  38081  fourierdlem14  38084  fourierdlem20  38090  fourierdlem25  38095  fourierdlem37  38108  fourierdlem41  38112  fourierdlem48  38119  fourierdlem49  38120  fourierdlem54  38125  fourierdlem64  38135  fourierdlem73  38144  fourierdlem79  38150  fourierdlem92  38163  fourierdlem93  38164  fourierdlem111  38182  sqwvfourb  38194  etransclem3  38203  etransclem7  38207  etransclem10  38210  etransclem15  38215  etransclem24  38224  etransclem25  38225  etransclem26  38226  etransclem27  38227  etransclem28  38228  etransclem35  38235  etransclem37  38237  etransclem38  38238  etransclem41  38241  etransclem44  38244  etransclem45  38245  etransclem48OLD  38248  etransclem48  38249  ovnsubaddlem1  38499  iccpartgtprec  38869  iccpartipre  38870  divgcdoddALTV  38946  perfectALTVlem1  38978  perfectALTVlem2  38979  perfectALTV  38980  gboge7  38999  proththdlem  39048  proththd  39049  pw2m1lepw2m1  40687  nnolog2flm1  40770  dignn0fr  40781  dignn0flhalflem1  40795