Theorem nnzd 9368

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

Syntax hints:   -> wi 4   e. wcel 2148   NNcn 8913   ZZcz 9247

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4119  ax-pow 4172  ax-pr 4207  ax-un 4431  ax-setind 4534  ax-cnex 7897  ax-resscn 7898  ax-1cn 7899  ax-1re 7900  ax-icn 7901  ax-addcl 7902  ax-addrcl 7903  ax-mulcl 7904  ax-addcom 7906  ax-addass 7908  ax-distr 7910  ax-i2m1 7911  ax-0lt1 7912  ax-0id 7914  ax-rnegex 7915  ax-cnre 7917  ax-pre-ltirr 7918  ax-pre-ltwlin 7919  ax-pre-lttrn 7920  ax-pre-ltadd 7922

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-int 3844  df-br 4002  df-opab 4063  df-id 4291  df-xp 4630  df-rel 4631  df-cnv 4632  df-co 4633  df-dm 4634  df-iota 5175  df-fun 5215  df-fv 5221  df-riota 5826  df-ov 5873  df-oprab 5874  df-mpo 5875  df-pnf 7988  df-mnf 7989  df-xr 7990  df-ltxr 7991  df-le 7992  df-sub 8124  df-neg 8125  df-inn 8914  df-n0 9171  df-z 9248

This theorem is referenced by:  qapne  9633  qtri3or  10236  exbtwnzlemstep  10241  modifeq2int  10379  modsumfzodifsn  10389  addmodlteq  10391  expnnval  10516  expnegap0  10521  expaddzaplem  10556  expmulzap  10559  facndiv  10710  bcval  10720  bcval5  10734  bcpasc  10737  caucvgre  10981  cvg1nlemcau  10984  cvg1nlemres  10985  resqrexlemdecn  11012  resqrexlemnmsq  11017  resqrexlemnm  11018  resqrexlemcvg  11019  resqrexlemoverl  11021  sumeq2  11358  nnf1o  11375  summodclem3  11379  summodclem2a  11380  summodclem2  11381  summodc  11382  zsumdc  11383  fsum3  11386  fisumss  11391  fsum3cvg3  11395  fsumcl2lem  11397  fsumadd  11405  sumsnf  11408  fsummulc2  11447  bcxmas  11488  geo2lim  11515  cvgratnnlembern  11522  cvgratnnlemseq  11525  cvgratnnlemabsle  11526  cvgratnnlemsumlt  11527  cvgratnnlemfm  11528  cvgratnnlemrate  11529  cvgratz  11531  mertenslemub  11533  mertenslemi1  11534  mertenslem2  11535  prodeq2  11556  prodmodclem3  11574  prodmodclem2a  11575  prodmodclem2  11576  fprodseq  11582  fprodssdc  11589  fprodmul  11590  prodsnf  11591  eftcl  11653  eftlub  11689  eirraplem  11775  dvdsle  11840  fzm1ndvds  11852  dvdsfac  11856  dvdsmod  11858  divalglemeunn  11916  gcddvds  11954  gcdnncl  11958  gcd1  11978  dvdsgcdidd  11985  bezoutlemnewy  11987  bezoutlemstep  11988  mulgcd  12007  gcdmultiplez  12012  rplpwr  12018  rppwr  12019  sqgcd  12020  dvdssq  12022  uzwodc  12028  lcmneg  12064  lcmgcdlem  12067  ncoprmgcdne1b  12079  rpdvds  12089  congr  12090  cncongr1  12093  cncongr2  12094  prmz  12101  prmind2  12110  divgcdodd  12133  isprm6  12137  prmexpb  12141  prmfac1  12142  rpexp  12143  sqrt2irrlem  12151  pw2dvdslemn  12155  pw2dvdseulemle  12157  oddpwdclemxy  12159  oddpwdclemodd  12162  sqpweven  12165  2sqpwodd  12166  sqrt2irraplemnn  12169  numdensq  12192  phivalfi  12202  hashdvds  12211  phiprmpw  12212  crth  12214  phimullem  12215  eulerthlem1  12217  eulerthlemfi  12218  eulerthlemrprm  12219  eulerthlema  12220  eulerthlemh  12221  eulerthlemth  12222  eulerth  12223  prmdivdiv  12227  hashgcdlem  12228  hashgcdeq  12229  phisum  12230  odzdvds  12235  powm2modprm  12242  pythagtriplem2  12256  pythagtriplem4  12258  pythagtriplem6  12260  pythagtriplem7  12261  pythagtriplem11  12264  pythagtriplem13  12266  pythagtriplem16  12269  pythagtriplem19  12272  pythagtrip  12273  pclemub  12277  pcprendvds2  12281  pcpre1  12282  pcpremul  12283  pceulem  12284  pcqmul  12293  pcdvdsb  12309  pcidlem  12312  pcdvdstr  12316  pcgcd1  12317  pc2dvds  12319  pcprmpw2  12322  pcaddlem  12328  pcadd  12329  pcmpt  12331  pcmpt2  12332  pcmptdvds  12333  pcprod  12334  pcfac  12338  pcbc  12339  qexpz  12340  oddprmdvds  12342  prmpwdvds  12343  pockthlem  12344  pockthg  12345  infpnlem2  12348  1arithlem4  12354  1arith  12355  4sqlem5  12370  4sqlem6  12371  4sqlem8  12373  4sqlem9  12374  4sqlem10  12375  oddennn  12383  exmidunben  12417  nninfdclemcl  12439  nninfdclemp1  12441  nninfdclemlt  12442  unbendc  12445  strleund  12552  mulgneg  12929  mulgnndir  12939  logbgcd1irraplemexp  14168  logbgcd1irraplemap  14169  lgsfvalg  14188  lgsfcl2  14189  lgsmod  14209  lgsdir  14218  lgsdilem2  14219  lgsne0  14221  2sqlem3  14235  2sqlem4  14236  2sqlem8  14241  2sqlem9  14242  cvgcmp2nlemabs  14551  trilpolemclim  14555  trilpolemisumle  14557  trilpolemeq1  14559  trilpolemlt1  14560  nconstwlpolemgt0  14582