Theorem nnzd 11936

Description: A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
nnzd.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnzd	⊢ (𝜑 → 𝐴 ∈ ℤ)

Proof of Theorem nnzd

Step	Hyp	Ref	Expression
1		nnzd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℕ)
2	1	nnnn0d 11805	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	2	nn0zd 11935	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2080  ℕcn 11488  ℤcz 11831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-sep 5097  ax-nul 5104  ax-pow 5160  ax-pr 5224  ax-un 7322  ax-1cn 10444  ax-icn 10445  ax-addcl 10446  ax-addrcl 10447  ax-mulcl 10448  ax-mulrcl 10449  ax-i2m1 10454  ax-1ne0 10455  ax-rnegex 10457  ax-rrecex 10458  ax-cnre 10459

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ne 2984  df-ral 3109  df-rex 3110  df-reu 3111  df-rab 3113  df-v 3438  df-sbc 3708  df-csb 3814  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-pss 3878  df-nul 4214  df-if 4384  df-pw 4457  df-sn 4475  df-pr 4477  df-tp 4479  df-op 4481  df-uni 4748  df-iun 4829  df-br 4965  df-opab 5027  df-mpt 5044  df-tr 5067  df-id 5351  df-eprel 5356  df-po 5365  df-so 5366  df-fr 5405  df-we 5407  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-rn 5457  df-res 5458  df-ima 5459  df-pred 6026  df-ord 6072  df-on 6073  df-lim 6074  df-suc 6075  df-iota 6192  df-fun 6230  df-fn 6231  df-f 6232  df-f1 6233  df-fo 6234  df-f1o 6235  df-fv 6236  df-ov 7022  df-om 7440  df-wrecs 7801  df-recs 7863  df-rdg 7901  df-neg 10722  df-nn 11489  df-n0 11748  df-z 11832

This theorem is referenced by:  expaddzlem  13322  expmulz  13325  expmulnbnd  13446  facndiv  13498  bcval5  13528  bcpasc  13531  hashf1  13663  isercolllem1  14855  isercolllem2  14856  o1fsum  15001  bcxmas  15023  climcndslem2  15038  climcnds  15039  mertenslem1  15073  fprodser  15136  bpolydiflem  15241  eftlub  15295  eirrlem  15390  rpnnen2lem7  15406  rpnnen2lem9  15408  rpnnen2lem11  15410  sqrt2irrlem  15434  dvdsfac  15509  dvdsmod  15511  oddpwp1fsum  15576  bitsfzolem  15616  bitsmod  15618  bitsfi  15619  bitscmp  15620  bitsinv1  15624  sadadd3  15643  sadaddlem  15648  bitsuz  15656  bitsshft  15657  gcdnncl  15689  gcd1  15709  bezoutlem3  15718  bezoutlem4  15719  mulgcd  15725  gcdmultiplez  15730  rplpwr  15736  rppwr  15737  sqgcd  15738  dvdssq  15740  lcmneg  15776  lcmgcdlem  15779  rpdvds  15833  coprmprod  15834  coprmproddvdslem  15835  congr  15837  cncongr1  15840  cncongr2  15841  prmz  15848  prmind2  15858  divgcdodd  15883  isprm6  15887  prmexpb  15891  prmfac1  15892  rpexp  15893  numdensq  15923  hashdvds  15941  phiprmpw  15942  crth  15944  phimullem  15945  eulerthlem1  15947  eulerthlem2  15948  prmdivdiv  15953  hashgcdlem  15954  odzdvds  15961  pythagtriplem4  15985  pythagtriplem6  15987  pythagtriplem7  15988  pythagtriplem11  15991  pythagtriplem13  15993  pythagtriplem19  15999  pclem  16004  pcprendvds2  16007  pcpre1  16008  pcpremul  16009  pceulem  16011  pcqmul  16019  pcdvdsb  16034  pcidlem  16037  pcdvdstr  16041  pcgcd1  16042  pc2dvds  16044  pcprmpw2  16047  pcaddlem  16053  pcadd  16054  pcmpt2  16058  pcmptdvds  16059  pcfac  16064  pcbc  16065  qexpz  16066  oddprmdvds  16068  prmpwdvds  16069  pockthlem  16070  pockthg  16071  prmreclem2  16082  prmreclem3  16083  prmreclem4  16084  prmreclem5  16085  prmreclem6  16086  4sqlem5  16107  4sqlem8  16110  4sqlem9  16111  4sqlem10  16112  4sqlem12  16121  4sqlem14  16123  4sqlem16  16125  4sqlem17  16126  vdwlem1  16146  vdwlem2  16147  vdwlem3  16148  vdwlem6  16151  vdwlem9  16154  vdwlem10  16155  vdwnnlem3  16162  prmdvdsprmop  16208  prmolelcmf  16213  prmgaplem1  16214  prmgaplem7  16222  prmgaplem8  16223  gsumwsubmcl  17814  gsumccat  17817  gsumwmhm  17821  mulgneg  18001  mulgnndir  18010  psgnunilem4  18356  odlem2  18398  mndodconglem  18400  odmod  18405  gexlem2  18437  gexcl3  18442  gexcl2  18444  sylow1lem1  18453  sylow1lem3  18455  sylow1lem5  18457  pgpfi  18460  fislw  18480  sylow3lem4  18485  gexexlem  18695  ablfacrplem  18904  ablfacrp  18905  ablfacrp2  18906  ablfac1lem  18907  ablfac1b  18909  ablfac1eu  18912  pgpfac1lem3a  18915  ablfaclem3  18926  znrrg  20394  cayhamlem1  21158  caublcls  23595  ovolicc2lem4  23804  iundisj2  23833  volsup  23840  uniioombllem3  23869  mbfi1fseqlem3  24001  mbfi1fseqlem4  24002  elqaalem2  24592  aalioulem1  24604  aalioulem4  24607  aalioulem5  24608  aalioulem6  24609  aaliou  24610  aaliou3lem1  24614  aaliou3lem2  24615  aaliou3lem3  24616  aaliou3lem8  24617  aaliou3lem5  24619  aaliou3lem6  24620  aaliou3lem7  24621  taylthlem2  24645  cxpeq  25019  amgmlem  25249  lgamgulmlem4  25291  lgamcvg2  25314  wilthlem2  25328  wilth  25330  wilthimp  25331  ftalem5  25336  basellem2  25341  basellem3  25342  basellem4  25343  basellem5  25344  muval1  25392  dvdssqf  25397  sgmnncl  25406  efchtdvds  25418  mumullem2  25439  mumul  25440  sqff1o  25441  fsumdvdsdiaglem  25442  dvdsppwf1o  25445  dvdsflf1o  25446  muinv  25452  dvdsmulf1o  25453  chtublem  25469  fsumvma2  25472  vmasum  25474  chpchtsum  25477  logfacubnd  25479  mersenne  25485  perfect1  25486  perfectlem1  25487  perfectlem2  25488  perfect  25489  dchrelbas4  25501  dchrfi  25513  bcmono  25535  bcp1ctr  25537  bclbnd  25538  bposlem1  25542  bposlem3  25544  bposlem5  25546  bposlem6  25547  bposlem9  25550  lgsmod  25581  lgsdir  25590  lgsdilem2  25591  lgsne0  25593  lgsqrlem2  25605  lgsqr  25609  lgsqrmodndvds  25611  gausslemma2dlem0c  25616  gausslemma2dlem0h  25621  gausslemma2dlem0i  25622  gausslemma2dlem2  25625  gausslemma2dlem6  25630  gausslemma2dlem7  25631  gausslemma2d  25632  lgseisenlem1  25633  lgseisenlem2  25634  lgseisenlem3  25635  lgseisenlem4  25636  lgsquadlem1  25638  lgsquadlem2  25639  lgsquadlem3  25640  lgsquad2lem1  25642  lgsquad2lem2  25643  lgsquad2  25644  m1lgs  25646  2lgslem2  25653  2sqlem3  25678  2sqlem4  25679  2sqlem8  25684  chebbnd1lem1  25727  rplogsumlem2  25743  rpvmasumlem  25745  dchrisumlem1  25747  dchrisumlem2  25748  dchrisumlem3  25749  dchrisum0fmul  25764  dchrisum0ff  25765  dchrisum0flblem1  25766  dchrisum0flblem2  25767  dchrisum0flb  25768  dchrisum0  25778  pntrsumbnd2  25825  pntrlog2bndlem1  25835  pntrlog2bndlem6  25841  pntpbnd2  25845  pntlemg  25856  pntlemj  25861  pntlemf  25863  ostth2lem2  25892  ostth2lem3  25893  ostth3  25896  numclwlk2lem2f1o  27842  minvecolem4  28340  iundisj2f  30022  ssnnssfz  30190  iundisj2fi  30198  f1ocnt  30201  prmdvdsbc  30208  numdenneg  30209  ltesubnnd  30214  isarchi3  30446  archiabllem1b  30451  psgnfzto1stlem  30656  smatrcl  30668  1smat1  30676  submateqlem1  30679  submateqlem2  30680  lmatfvlem  30687  qqhval2  30832  qqhf  30836  qqhghm  30838  qqhrhm  30839  qqhnm  30840  qqhre  30870  esumcvg  30954  meascnbl  31087  omssubadd  31167  oddpwdc  31221  ballotlemfp1  31358  ballotlemfc0  31359  ballotlemfcc  31360  ballotlemimin  31372  ballotlemic  31373  ballotlem1c  31374  hgt750lemc  31527  hgt750lemd  31528  hgt750lemb  31536  hgt750leme  31538  subfaclim  32037  cvmliftlem7  32140  sinccvglem  32517  bcprod  32572  bccolsum  32573  faclimlem2  32578  faclim2  32582  poimirlem1  34437  poimirlem2  34438  poimirlem3  34439  poimirlem4  34440  poimirlem6  34442  poimirlem8  34444  poimirlem9  34445  poimirlem10  34446  poimirlem11  34447  poimirlem13  34449  poimirlem14  34450  poimirlem15  34451  poimirlem16  34452  poimirlem17  34453  poimirlem18  34454  poimirlem19  34455  poimirlem20  34456  poimirlem21  34457  poimirlem22  34458  poimirlem23  34459  poimirlem24  34460  poimirlem26  34462  poimirlem27  34463  poimirlem28  34464  poimirlem31  34467  mblfinlem2  34474  seqpo  34567  incsequz  34568  incsequz2  34569  oexpreposd  38714  expgcd  38718  nn0expgcd  38719  numdenexp  38721  zrtelqelz  38727  fltne  38782  fltltc  38783  fltnlta  38785  irrapxlem3  38919  irrapxlem5  38921  pellexlem5  38928  pellexlem6  38929  pellex  38930  pell1234qrmulcl  38950  jm2.23  39091  jm2.20nn  39092  jm2.26lem3  39096  jm2.27a  39100  jm2.27b  39101  jm2.27c  39102  jm3.1lem1  39112  jm3.1lem3  39114  inductionexd  40003  gcddvdsd  40072  fincygsubgd  40181  fincygsubgodd  40182  nznngen  40199  hashnzfz2  40204  fmuldfeq  41419  divcnvg  41463  stoweidlem1  41842  stoweidlem3  41844  stoweidlem11  41852  stoweidlem20  41861  stoweidlem26  41867  stoweidlem34  41875  stoweidlem51  41892  stirlinglem4  41918  stirlinglem5  41919  stirlinglem8  41922  dirkerper  41937  dirkertrigeqlem2  41940  dirkertrigeqlem3  41941  dirkercncflem2  41945  fourierdlem11  41959  fourierdlem14  41962  fourierdlem20  41968  fourierdlem25  41973  fourierdlem37  41985  fourierdlem41  41989  fourierdlem48  41995  fourierdlem49  41996  fourierdlem54  42001  fourierdlem64  42011  fourierdlem73  42020  fourierdlem79  42026  fourierdlem92  42039  fourierdlem93  42040  fourierdlem111  42058  sqwvfourb  42070  etransclem3  42078  etransclem7  42082  etransclem10  42085  etransclem15  42090  etransclem24  42099  etransclem25  42100  etransclem26  42101  etransclem27  42102  etransclem28  42103  etransclem35  42110  etransclem37  42112  etransclem38  42113  etransclem41  42116  etransclem44  42119  etransclem45  42120  etransclem48  42123  ovnsubaddlem1  42408  vonioolem1  42518  iccpartgtprec  43076  iccpartipre  43077  fmtnoodd  43191  goldbachthlem2  43204  goldbachth  43205  odz2prm2pw  43221  fmtnoprmfac1lem  43222  fmtnoprmfac2lem1  43224  fmtnoprmfac2  43225  fmtnofac2lem  43226  2pwp1prm  43247  lighneallem1  43266  lighneallem4  43271  proththdlem  43274  proththd  43275  divgcdoddALTV  43343  perfectALTVlem1  43382  perfectALTVlem2  43383  perfectALTV  43384  gbowge7  43424  pw2m1lepw2m1  44070  nnolog2flm1  44145  dignn0fr  44156  dignn0flhalflem1  44170