Theorem nnzd 12585

Description: A positive 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 12532	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	2	nn0zd 12584	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2107  ℕcn 12212  ℤcz 12558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-i2m1 11178  ax-1ne0 11179  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-neg 11447  df-nn 12213  df-n0 12473  df-z 12559

This theorem is referenced by:  expaddzlem  14071  expmulz  14074  expmulnbnd  14198  facndiv  14248  bcval5  14278  bcpasc  14281  hashf1  14418  isercolllem1  15611  isercolllem2  15612  o1fsum  15759  bcxmas  15781  climcndslem2  15796  climcnds  15797  mertenslem1  15830  fprodser  15893  bpolydiflem  15998  eftlub  16052  eirrlem  16147  rpnnen2lem7  16163  rpnnen2lem9  16165  rpnnen2lem11  16167  sqrt2irrlem  16191  dvdsfac  16269  dvdsmod  16272  oddpwp1fsum  16335  bitsfzolem  16375  bitsmod  16377  bitsfi  16378  bitscmp  16379  bitsinv1  16383  sadadd3  16402  sadaddlem  16407  bitsuz  16415  bitsshft  16416  gcdnncl  16448  gcd1  16469  dvdsgcdidd  16479  bezoutlem3  16483  bezoutlem4  16484  mulgcd  16490  rplpwr  16499  rprpwr  16500  sqgcd  16502  dvdssq  16504  lcmneg  16540  lcmgcdlem  16543  rpdvds  16597  coprmprod  16598  coprmproddvdslem  16599  congr  16601  cncongr1  16604  cncongr2  16605  prmz  16612  prmind2  16622  divgcdodd  16647  isprm6  16651  prmexpb  16657  prmfac1  16658  rpexp  16659  prmdvdsncoprmbd  16663  numdensq  16690  hashdvds  16708  phiprmpw  16709  crth  16711  phimullem  16712  eulerthlem1  16714  eulerthlem2  16715  prmdivdiv  16720  hashgcdlem  16721  odzdvds  16728  pythagtriplem4  16752  pythagtriplem6  16754  pythagtriplem7  16755  pythagtriplem11  16758  pythagtriplem13  16760  pythagtriplem19  16766  pclem  16771  pcprendvds2  16774  pcpre1  16775  pcpremul  16776  pceulem  16778  pcqmul  16786  pcdvdsb  16802  pcidlem  16805  pcdvdstr  16809  pcgcd1  16810  pc2dvds  16812  pcprmpw2  16815  pcaddlem  16821  pcadd  16822  pcmpt2  16826  pcmptdvds  16827  pcfac  16832  pcbc  16833  qexpz  16834  oddprmdvds  16836  prmpwdvds  16837  pockthlem  16838  pockthg  16839  prmreclem2  16850  prmreclem3  16851  prmreclem4  16852  prmreclem5  16853  prmreclem6  16854  4sqlem5  16875  4sqlem8  16878  4sqlem9  16879  4sqlem10  16880  4sqlem12  16889  4sqlem14  16891  4sqlem16  16893  4sqlem17  16894  vdwlem1  16914  vdwlem2  16915  vdwlem3  16916  vdwlem6  16919  vdwlem9  16922  vdwlem10  16923  vdwnnlem3  16930  prmdvdsprmop  16976  prmolelcmf  16981  prmgaplem1  16982  prmgaplem7  16990  prmgaplem8  16991  gsumwsubmcl  18718  gsumsgrpccat  18721  gsumwmhm  18726  mulgneg  18972  mulgnndir  18983  psgnunilem4  19365  odlem2  19407  mndodconglem  19409  odmod  19414  gexlem2  19450  gexcl3  19455  gexcl2  19457  sylow1lem1  19466  sylow1lem3  19468  sylow1lem5  19470  pgpfi  19473  fislw  19493  sylow3lem4  19498  gexexlem  19720  ablfacrplem  19935  ablfacrp  19936  ablfacrp2  19937  ablfac1lem  19938  ablfac1b  19940  ablfac1eu  19943  pgpfac1lem3a  19946  ablfaclem3  19957  fincygsubgd  19981  fincygsubgodd  19982  znrrg  21121  cayhamlem1  22368  caublcls  24826  ovolicc2lem4  25037  iundisj2  25066  volsup  25073  uniioombllem3  25102  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  elqaalem2  25833  aalioulem1  25845  aalioulem4  25848  aalioulem5  25849  aalioulem6  25850  aaliou  25851  aaliou3lem1  25855  aaliou3lem2  25856  aaliou3lem3  25857  aaliou3lem8  25858  aaliou3lem5  25860  aaliou3lem6  25861  aaliou3lem7  25862  taylthlem2  25886  cxpeq  26265  amgmlem  26494  lgamgulmlem4  26536  lgamcvg2  26559  wilthlem2  26573  wilth  26575  wilthimp  26576  ftalem5  26581  basellem2  26586  basellem3  26587  basellem4  26588  basellem5  26589  muval1  26637  dvdssqf  26642  sgmnncl  26651  efchtdvds  26663  mumullem2  26684  mumul  26685  sqff1o  26686  fsumdvdsdiaglem  26687  dvdsppwf1o  26690  dvdsflf1o  26691  muinv  26697  dvdsmulf1o  26698  chtublem  26714  fsumvma2  26717  vmasum  26719  chpchtsum  26722  logfacubnd  26724  mersenne  26730  perfect1  26731  perfectlem1  26732  perfectlem2  26733  perfect  26734  dchrelbas4  26746  dchrfi  26758  bcmono  26780  bcp1ctr  26782  bclbnd  26783  bposlem1  26787  bposlem3  26789  bposlem5  26791  bposlem6  26792  bposlem9  26795  lgsmod  26826  lgsdir  26835  lgsdilem2  26836  lgsne0  26838  lgsqrlem2  26850  lgsqr  26854  lgsqrmodndvds  26856  gausslemma2dlem0c  26861  gausslemma2dlem0h  26866  gausslemma2dlem0i  26867  gausslemma2dlem2  26870  gausslemma2dlem6  26875  gausslemma2dlem7  26876  gausslemma2d  26877  lgseisenlem1  26878  lgseisenlem2  26879  lgseisenlem3  26880  lgseisenlem4  26881  lgsquadlem1  26883  lgsquadlem2  26884  lgsquadlem3  26885  lgsquad2lem1  26887  lgsquad2lem2  26888  lgsquad2  26889  m1lgs  26891  2lgslem2  26898  2sqlem3  26923  2sqlem4  26924  2sqlem8  26929  chebbnd1lem1  26972  rplogsumlem2  26988  rpvmasumlem  26990  dchrisumlem1  26992  dchrisumlem2  26993  dchrisumlem3  26994  dchrisum0fmul  27009  dchrisum0ff  27010  dchrisum0flblem1  27011  dchrisum0flblem2  27012  dchrisum0flb  27013  dchrisum0  27023  pntrsumbnd2  27070  pntrlog2bndlem1  27080  pntrlog2bndlem6  27086  pntpbnd2  27090  pntlemg  27101  pntlemj  27106  pntlemf  27108  ostth2lem2  27137  ostth2lem3  27138  ostth3  27141  numclwlk2lem2f1o  29632  nrt2irr  29726  minvecolem4  30133  iundisj2f  31821  ssnnssfz  31998  iundisj2fi  32008  f1ocnt  32013  prmdvdsbc  32022  numdenneg  32023  ltesubnnd  32028  psgnfzto1stlem  32259  isarchi3  32333  archiabllem1b  32338  smatrcl  32776  1smat1  32784  submateqlem1  32787  lmatfvlem  32795  qqhval2  32962  qqhf  32966  qqhghm  32968  qqhrhm  32969  qqhnm  32970  qqhre  33000  esumcvg  33084  meascnbl  33217  omssubadd  33299  oddpwdc  33353  ballotlemfp1  33490  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemimin  33504  ballotlemic  33505  ballotlem1c  33506  hgt750lemc  33659  hgt750lemd  33660  hgt750lemb  33668  hgt750leme  33670  subfaclim  34179  cvmliftlem7  34282  sinccvglem  34657  bcprod  34708  bccolsum  34709  faclimlem2  34714  faclim2  34718  poimirlem1  36489  poimirlem2  36490  poimirlem3  36491  poimirlem4  36492  poimirlem6  36494  poimirlem8  36496  poimirlem9  36497  poimirlem10  36498  poimirlem11  36499  poimirlem13  36501  poimirlem14  36502  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem18  36506  poimirlem19  36507  poimirlem20  36508  poimirlem21  36509  poimirlem22  36510  poimirlem23  36511  poimirlem24  36512  poimirlem26  36514  poimirlem27  36515  poimirlem28  36516  poimirlem31  36519  mblfinlem2  36526  seqpo  36615  incsequz  36616  incsequz2  36617  bccl2d  40857  nnproddivdvdsd  40866  lcmineqlem1  40894  lcmineqlem3  40896  lcmineqlem4  40897  lcmineqlem6  40899  lcmineqlem8  40901  lcmineqlem9  40902  lcmineqlem10  40903  lcmineqlem11  40904  lcmineqlem13  40906  lcmineqlem14  40907  lcmineqlem18  40911  lcmineqlem19  40912  lcmineqlem20  40913  lcmineqlem21  40914  lcmineqlem22  40915  lcmineqlem23  40916  lcmineqlem  40917  3lexlogpow5ineq2  40920  3lexlogpow2ineq1  40923  aks4d1p3  40943  aks4d1p5  40945  aks4d1p6  40946  aks4d1p8d1  40949  aks4d1p8d2  40950  aks4d1p8d3  40951  aks4d1p8  40952  aks4d1p9  40953  aks6d1c2p2  40957  sticksstones6  40967  sticksstones10  40971  sticksstones12a  40973  sticksstones12  40974  metakunt1  40985  metakunt2  40986  metakunt3  40987  metakunt4  40988  metakunt5  40989  metakunt7  40991  metakunt10  40994  metakunt15  40999  metakunt16  41000  metakunt18  41002  metakunt19  41003  metakunt20  41004  metakunt21  41005  metakunt22  41006  metakunt24  41008  metakunt25  41009  metakunt26  41010  metakunt27  41011  metakunt28  41012  metakunt29  41013  metakunt30  41014  metakunt32  41016  metakunt33  41017  sumcubes  41211  oexpreposd  41212  exp11d  41216  gcdle1d  41221  gcdle2d  41222  expgcd  41225  nn0expgcd  41226  numdenexp  41228  dvdsexpnn0  41232  zrtelqelz  41235  fltdvdsabdvdsc  41380  fltaccoprm  41382  fltbccoprm  41383  fltabcoprm  41384  fltne  41386  flt4lem2  41389  flt4lem3  41390  flt4lem4  41391  flt4lem5  41392  flt4lem5elem  41393  flt4lem5a  41394  flt4lem5b  41395  flt4lem5c  41396  flt4lem5d  41397  flt4lem5e  41398  flt4lem5f  41399  flt4lem6  41400  flt4lem7  41401  nna4b4nsq  41402  fltltc  41403  fltnlta  41405  irrapxlem3  41562  irrapxlem5  41564  pellexlem5  41571  pellexlem6  41572  pellex  41573  pell1234qrmulcl  41593  jm2.23  41735  jm2.20nn  41736  jm2.26lem3  41740  jm2.27a  41744  jm2.27b  41745  jm2.27c  41746  jm3.1lem1  41756  jm3.1lem3  41758  inductionexd  42906  nznngen  43075  hashnzfz2  43080  fmuldfeq  44299  divcnvg  44343  stoweidlem1  44717  stoweidlem3  44719  stoweidlem11  44727  stoweidlem20  44736  stoweidlem26  44742  stoweidlem34  44750  stoweidlem51  44767  stirlinglem4  44793  stirlinglem5  44794  stirlinglem8  44797  dirkerper  44812  dirkertrigeqlem2  44815  dirkertrigeqlem3  44816  dirkercncflem2  44820  fourierdlem11  44834  fourierdlem14  44837  fourierdlem20  44843  fourierdlem25  44848  fourierdlem37  44860  fourierdlem41  44864  fourierdlem48  44870  fourierdlem49  44871  fourierdlem54  44876  fourierdlem64  44886  fourierdlem73  44895  fourierdlem79  44901  fourierdlem92  44914  fourierdlem93  44915  fourierdlem111  44933  sqwvfourb  44945  etransclem3  44953  etransclem7  44957  etransclem10  44960  etransclem15  44965  etransclem24  44974  etransclem25  44975  etransclem26  44976  etransclem27  44977  etransclem28  44978  etransclem35  44985  etransclem37  44987  etransclem38  44988  etransclem41  44991  etransclem44  44994  etransclem45  44995  etransclem48  44998  ovnsubaddlem1  45286  vonioolem1  45396  iccpartgtprec  46088  iccpartipre  46089  fmtnoodd  46201  goldbachthlem2  46214  goldbachth  46215  odz2prm2pw  46231  fmtnoprmfac1lem  46232  fmtnoprmfac2lem1  46234  fmtnoprmfac2  46235  fmtnofac2lem  46236  2pwp1prm  46257  lighneallem1  46273  lighneallem4  46278  proththdlem  46281  proththd  46282  divgcdoddALTV  46350  perfectALTVlem1  46389  perfectALTVlem2  46390  perfectALTV  46391  gbowge7  46431  pw2m1lepw2m1  47201  nnolog2flm1  47276  dignn0fr  47287  dignn0flhalflem1  47301