Theorem nnzd 10734

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

Syntax hints:   -> wi 4   e. wcel 1755   NNcn 10310   ZZcz 10634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-mulcom 9334  ax-addass 9335  ax-mulass 9336  ax-distr 9337  ax-i2m1 9338  ax-1ne0 9339  ax-1rid 9340  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343  ax-pre-lttri 9344  ax-pre-lttrn 9345  ax-pre-ltadd 9346  ax-pre-mulgt0 9347

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-om 6466  df-recs 6818  df-rdg 6852  df-er 7089  df-en 7299  df-dom 7300  df-sdom 7301  df-pnf 9408  df-mnf 9409  df-xr 9410  df-ltxr 9411  df-le 9412  df-sub 9585  df-neg 9586  df-nn 10311  df-n0 10568  df-z 10635

This theorem is referenced by:  expaddzlem  11891  expmulz  11894  expmulnbnd  11980  facndiv  12048  bcval5  12078  bcpasc  12081  hashf1  12194  isercolllem1  13126  isercolllem2  13127  o1fsum  13259  bcxmas  13281  climcndslem2  13296  climcnds  13297  mertenslem1  13327  eftlub  13376  eirrlem  13469  rpnnen2lem7  13486  rpnnen2lem9  13488  rpnnen2lem11  13490  sqr2irrlem  13513  dvdsfac  13571  dvdsmod  13573  bitsfzolem  13613  bitsmod  13615  bitsfi  13616  bitscmp  13617  bitsinv1  13621  sadadd3  13640  sadaddlem  13645  bitsuz  13653  bitsshft  13654  gcd1  13699  bezoutlem3  13707  bezoutlem4  13708  mulgcd  13713  gcdmultiplez  13718  rplpwr  13723  rppwr  13724  sqgcd  13725  dvdssq  13727  prmz  13750  prmind2  13757  isprm6  13778  prmexpb  13786  prmfac1  13787  divgcdodd  13788  rpexp  13789  rpdvds  13793  numdensq  13815  hashdvds  13833  phiprmpw  13834  crt  13836  phimullem  13837  eulerthlem1  13839  eulerthlem2  13840  prmdivdiv  13845  odzdvds  13850  pythagtriplem4  13869  pythagtriplem6  13871  pythagtriplem7  13872  pythagtriplem11  13875  pythagtriplem13  13877  pythagtriplem19  13883  pclem  13888  pcprendvds2  13891  pcpre1  13892  pcpremul  13893  pceulem  13895  pcqmul  13903  pcdvdsb  13918  pcidlem  13921  pcdvdstr  13925  pcgcd1  13926  pc2dvds  13928  pcprmpw2  13931  pcaddlem  13933  pcadd  13934  pcmpt2  13938  pcmptdvds  13939  pcfac  13944  pcbc  13945  qexpz  13946  prmpwdvds  13948  pockthlem  13949  pockthg  13950  prmreclem2  13961  prmreclem3  13962  prmreclem4  13963  prmreclem5  13964  prmreclem6  13965  4sqlem5  13986  4sqlem8  13989  4sqlem9  13990  4sqlem10  13991  4sqlem12  14000  4sqlem14  14002  4sqlem16  14004  4sqlem17  14005  vdwlem1  14025  vdwlem2  14026  vdwlem3  14027  vdwlem6  14030  vdwlem9  14033  vdwlem10  14034  vdwnnlem3  14041  gsumwsubmcl  15496  gsumccat  15499  gsumwmhm  15503  mulgneg  15625  mulgnndir  15629  psgnunilem4  15983  odlem2  16022  mndodconglem  16024  odmod  16029  gexlem2  16061  gexcl3  16066  gexcl2  16068  sylow1lem1  16077  sylow1lem3  16079  sylow1lem5  16081  pgpfi  16084  fislw  16104  sylow3lem4  16109  gexexlem  16314  ablfacrplem  16540  ablfacrp  16541  ablfacrp2  16542  ablfac1lem  16543  ablfac1b  16545  ablfac1eu  16548  pgpfac1lem3a  16551  ablfaclem3  16562  caublcls  20661  ovolicc2lem4  20845  iundisj2  20872  volsup  20879  uniioombllem3  20907  mbfi1fseqlem3  21037  mbfi1fseqlem4  21038  elqaalem2  21671  aalioulem1  21683  aalioulem4  21686  aalioulem5  21687  aalioulem6  21688  aaliou  21689  aaliou3lem1  21693  aaliou3lem2  21694  aaliou3lem3  21695  aaliou3lem8  21696  aaliou3lem5  21698  aaliou3lem6  21699  aaliou3lem7  21700  taylthlem2  21724  cxpeq  22080  amgmlem  22268  wilthlem2  22292  wilth  22294  ftalem5  22299  basellem2  22304  basellem3  22305  basellem4  22306  basellem5  22307  muval1  22356  dvdssqf  22361  sgmnncl  22370  efchtdvds  22382  mumullem2  22403  mumul  22404  sqff1o  22405  fsumdvdsdiaglem  22408  dvdsppwf1o  22411  dvdsflf1o  22412  muinv  22418  dvdsmulf1o  22419  chtublem  22435  fsumvma2  22438  vmasum  22440  chpchtsum  22443  logfacubnd  22445  mersenne  22451  perfect1  22452  perfectlem1  22453  perfectlem2  22454  perfect  22455  dchrelbas4  22467  dchrfi  22479  bcmono  22501  bcp1ctr  22503  bclbnd  22504  bposlem1  22508  bposlem3  22510  bposlem5  22512  bposlem6  22513  bposlem9  22516  lgsmod  22545  lgsdir  22554  lgsdilem2  22555  lgsne0  22557  lgsqrlem2  22566  lgsqr  22570  lgseisenlem1  22573  lgseisenlem2  22574  lgseisenlem3  22575  lgseisenlem4  22576  lgsquadlem1  22578  lgsquadlem2  22579  lgsquadlem3  22580  lgsquad2lem1  22582  lgsquad2lem2  22583  lgsquad2  22584  m1lgs  22586  2sqlem3  22590  2sqlem4  22591  2sqlem8  22596  chebbnd1lem1  22603  rplogsumlem2  22619  rpvmasumlem  22621  dchrisumlem1  22623  dchrisumlem2  22624  dchrisumlem3  22625  dchrisum0fmul  22640  dchrisum0ff  22641  dchrisum0flblem1  22642  dchrisum0flblem2  22643  dchrisum0flb  22644  dchrisum0  22654  pntrsumbnd2  22701  pntrlog2bndlem1  22711  pntrlog2bndlem6  22717  pntpbnd2  22721  pntlemg  22732  pntlemj  22737  pntlemf  22739  ostth2lem2  22768  ostth2lem3  22769  ostth3  22772  minvecolem4  24104  iundisj2f  25756  ssnnssfz  25899  iundisj2fi  25904  numdenneg  25909  ltesubnnd  25914  isarchi3  26028  qqhval2  26265  qqhf  26269  qqhghm  26271  qqhrhm  26272  qqhnm  26273  qqhre  26300  esumcvg  26389  meascnbl  26487  oddpwdc  26585  ballotlemfp1  26722  ballotlemfc0  26723  ballotlemfcc  26724  ballotlemimin  26736  ballotlemic  26737  ballotlem1c  26738  lgamgulmlem4  26866  lgamcvg2  26889  subfaclim  26924  cvmliftlem7  27028  sinccvglem  27164  fprodser  27309  faclimlem2  27397  faclim2  27401  bpolydiflem  28044  mblfinlem2  28273  seqpo  28487  incsequz  28488  incsequz2  28489  irrapxlem3  29010  irrapxlem5  29012  pellexlem5  29019  pellexlem6  29020  pellex  29021  pell1234qrmulcl  29041  jm2.23  29190  jm2.20nn  29191  jm2.26lem3  29195  jm2.27a  29199  jm2.27b  29200  jm2.27c  29201  jm3.1lem1  29211  jm3.1lem3  29213  hashgcdlem  29410  fmuldfeq  29609  stoweidlem1  29642  stoweidlem3  29644  stoweidlem11  29652  stoweidlem20  29661  stoweidlem26  29667  stoweidlem34  29675  stoweidlem51  29692  stirlinglem4  29718  stirlinglem5  29719  stirlinglem8  29722