Theorem nnzd 9409

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

Syntax hints:   -> wi 4   e. wcel 2160   NNcn 8954   ZZcz 9288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4139  ax-pow 4195  ax-pr 4230  ax-un 4454  ax-setind 4557  ax-cnex 7937  ax-resscn 7938  ax-1cn 7939  ax-1re 7940  ax-icn 7941  ax-addcl 7942  ax-addrcl 7943  ax-mulcl 7944  ax-addcom 7946  ax-addass 7948  ax-distr 7950  ax-i2m1 7951  ax-0lt1 7952  ax-0id 7954  ax-rnegex 7955  ax-cnre 7957  ax-pre-ltirr 7958  ax-pre-ltwlin 7959  ax-pre-lttrn 7960  ax-pre-ltadd 7962

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-pw 3595  df-sn 3616  df-pr 3617  df-op 3619  df-uni 3828  df-int 3863  df-br 4022  df-opab 4083  df-id 4314  df-xp 4653  df-rel 4654  df-cnv 4655  df-co 4656  df-dm 4657  df-iota 5199  df-fun 5240  df-fv 5246  df-riota 5855  df-ov 5903  df-oprab 5904  df-mpo 5905  df-pnf 8029  df-mnf 8030  df-xr 8031  df-ltxr 8032  df-le 8033  df-sub 8165  df-neg 8166  df-inn 8955  df-n0 9212  df-z 9289

This theorem is referenced by:  qapne  9675  qtri3or  10279  exbtwnzlemstep  10284  modifeq2int  10423  modsumfzodifsn  10433  addmodlteq  10435  expnnval  10563  expnegap0  10568  expaddzaplem  10603  expmulzap  10606  facndiv  10760  bcval  10770  bcval5  10784  bcpasc  10787  caucvgre  11031  cvg1nlemcau  11034  cvg1nlemres  11035  resqrexlemdecn  11062  resqrexlemnmsq  11067  resqrexlemnm  11068  resqrexlemcvg  11069  resqrexlemoverl  11071  sumeq2  11408  nnf1o  11425  summodclem3  11429  summodclem2a  11430  summodclem2  11431  summodc  11432  zsumdc  11433  fsum3  11436  fisumss  11441  fsum3cvg3  11445  fsumcl2lem  11447  fsumadd  11455  sumsnf  11458  fsummulc2  11497  bcxmas  11538  geo2lim  11565  cvgratnnlembern  11572  cvgratnnlemseq  11575  cvgratnnlemabsle  11576  cvgratnnlemsumlt  11577  cvgratnnlemfm  11578  cvgratnnlemrate  11579  cvgratz  11581  mertenslemub  11583  mertenslemi1  11584  mertenslem2  11585  prodeq2  11606  prodmodclem3  11624  prodmodclem2a  11625  prodmodclem2  11626  fprodseq  11632  fprodssdc  11639  fprodmul  11640  prodsnf  11641  eftcl  11703  eftlub  11739  eirraplem  11825  dvdsle  11891  fzm1ndvds  11903  dvdsfac  11907  dvdsmod  11909  divalglemeunn  11967  gcddvds  12005  gcdnncl  12009  gcd1  12029  dvdsgcdidd  12036  bezoutlemnewy  12038  bezoutlemstep  12039  mulgcd  12058  gcdmultiplez  12063  rplpwr  12069  rppwr  12070  sqgcd  12071  dvdssq  12073  uzwodc  12079  lcmneg  12117  lcmgcdlem  12120  ncoprmgcdne1b  12132  rpdvds  12142  congr  12143  cncongr1  12146  cncongr2  12147  prmz  12154  prmind2  12163  divgcdodd  12186  isprm6  12190  prmexpb  12194  prmfac1  12195  rpexp  12196  sqrt2irrlem  12204  pw2dvdslemn  12208  pw2dvdseulemle  12210  oddpwdclemxy  12212  oddpwdclemodd  12215  sqpweven  12218  2sqpwodd  12219  sqrt2irraplemnn  12222  numdensq  12245  phivalfi  12255  hashdvds  12264  phiprmpw  12265  crth  12267  phimullem  12268  eulerthlem1  12270  eulerthlemfi  12271  eulerthlemrprm  12272  eulerthlema  12273  eulerthlemh  12274  eulerthlemth  12275  eulerth  12276  prmdivdiv  12280  hashgcdlem  12281  hashgcdeq  12282  phisum  12283  odzdvds  12288  powm2modprm  12295  pythagtriplem2  12309  pythagtriplem4  12311  pythagtriplem6  12313  pythagtriplem7  12314  pythagtriplem11  12317  pythagtriplem13  12319  pythagtriplem16  12322  pythagtriplem19  12325  pythagtrip  12326  pclemub  12330  pcprendvds2  12334  pcpre1  12335  pcpremul  12336  pceulem  12337  pcqmul  12346  pcdvdsb  12363  pcidlem  12366  pcdvdstr  12370  pcgcd1  12371  pc2dvds  12373  pcprmpw2  12376  pcaddlem  12382  pcadd  12383  pcmpt  12386  pcmpt2  12387  pcmptdvds  12388  pcprod  12389  pcfac  12393  pcbc  12394  qexpz  12395  oddprmdvds  12397  prmpwdvds  12398  pockthlem  12399  pockthg  12400  infpnlem2  12403  1arithlem4  12409  1arith  12410  4sqlem5  12425  4sqlem6  12426  4sqlem8  12428  4sqlem9  12429  4sqlem10  12430  4sqlemafi  12438  4sqlemffi  12439  4sqleminfi  12440  4sqlem11  12444  4sqlem12  12445  4sqlem14  12447  4sqlem16  12449  4sqlem17  12450  oddennn  12454  exmidunben  12488  nninfdclemcl  12510  nninfdclemp1  12512  nninfdclemlt  12513  unbendc  12516  strleund  12626  mulgneg  13105  mulgnndir  13116  logbgcd1irraplemexp  14871  logbgcd1irraplemap  14872  lgsfvalg  14892  lgsfcl2  14893  lgsmod  14913  lgsdir  14922  lgsdilem2  14923  lgsne0  14925  lgseisenlem1  14936  lgseisenlem2  14937  m1lgs  14938  2sqlem3  14950  2sqlem4  14951  2sqlem8  14956  2sqlem9  14957  cvgcmp2nlemabs  15268  trilpolemclim  15272  trilpolemisumle  15274  trilpolemeq1  15276  trilpolemlt1  15277  nconstwlpolemgt0  15300