Theorem nnzd 12556

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 12503	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	2	nn0zd 12555	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2109  ℕcn 12186  ℤcz 12529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-neg 11408  df-nn 12187  df-n0 12443  df-z 12530

This theorem is referenced by:  expaddzlem  14070  expmulz  14073  expmulnbnd  14200  facndiv  14253  bcval5  14283  bcpasc  14286  hashf1  14422  isercolllem1  15631  isercolllem2  15632  o1fsum  15779  bcxmas  15801  climcndslem2  15816  climcnds  15817  mertenslem1  15850  fprodser  15915  bpolydiflem  16020  eftlub  16077  eirrlem  16172  rpnnen2lem7  16188  rpnnen2lem9  16190  rpnnen2lem11  16192  sqrt2irrlem  16216  dvdsfac  16296  dvdsmod  16299  oddpwp1fsum  16362  bitsfzolem  16404  bitsmod  16406  bitsfi  16407  bitscmp  16408  bitsinv1  16412  sadadd3  16431  sadaddlem  16436  bitsuz  16444  bitsshft  16445  gcdnncl  16477  gcd1  16498  dvdsgcdidd  16507  bezoutlem3  16511  bezoutlem4  16512  mulgcd  16518  rplpwr  16528  rprpwr  16529  sqgcd  16532  expgcd  16533  nn0expgcd  16534  dvdssq  16537  lcmneg  16573  lcmgcdlem  16576  rpdvds  16630  coprmprod  16631  coprmproddvdslem  16632  congr  16634  cncongr1  16637  cncongr2  16638  prmz  16645  prmind2  16655  divgcdodd  16680  isprm6  16684  prmexpb  16689  prmfac1  16690  rpexp  16692  prmdvdsbc  16696  prmdvdsncoprmbd  16697  numdensq  16724  numdenexp  16730  hashdvds  16745  phiprmpw  16746  crth  16748  phimullem  16749  eulerthlem1  16751  eulerthlem2  16752  prmdivdiv  16757  hashgcdlem  16758  odzdvds  16766  pythagtriplem4  16790  pythagtriplem6  16792  pythagtriplem7  16793  pythagtriplem11  16796  pythagtriplem13  16798  pythagtriplem19  16804  pclem  16809  pcprendvds2  16812  pcpre1  16813  pcpremul  16814  pceulem  16816  pcqmul  16824  pcdvdsb  16840  pcidlem  16843  pcdvdstr  16847  pcgcd1  16848  pc2dvds  16850  pcprmpw2  16853  pcaddlem  16859  pcadd  16860  pcmpt2  16864  pcmptdvds  16865  pcfac  16870  pcbc  16871  qexpz  16872  oddprmdvds  16874  prmpwdvds  16875  pockthlem  16876  pockthg  16877  prmreclem2  16888  prmreclem3  16889  prmreclem4  16890  prmreclem5  16891  prmreclem6  16892  4sqlem5  16913  4sqlem8  16916  4sqlem9  16917  4sqlem10  16918  4sqlem12  16927  4sqlem14  16929  4sqlem16  16931  4sqlem17  16932  vdwlem1  16952  vdwlem2  16953  vdwlem3  16954  vdwlem6  16957  vdwlem9  16960  vdwlem10  16961  vdwnnlem3  16968  prmdvdsprmop  17014  prmolelcmf  17019  prmgaplem1  17020  prmgaplem7  17028  prmgaplem8  17029  gsumwsubmcl  18764  gsumsgrpccat  18767  gsumwmhm  18772  mulgneg  19024  mulgnndir  19035  psgnunilem4  19427  odlem2  19469  mndodconglem  19471  odmod  19476  gexlem2  19512  gexcl3  19517  gexcl2  19519  sylow1lem1  19528  sylow1lem3  19530  sylow1lem5  19532  pgpfi  19535  fislw  19555  sylow3lem4  19560  gexexlem  19782  ablfacrplem  19997  ablfacrp  19998  ablfacrp2  19999  ablfac1lem  20000  ablfac1b  20002  ablfac1eu  20005  pgpfac1lem3a  20008  ablfaclem3  20019  fincygsubgd  20043  fincygsubgodd  20044  znrrg  21475  psdpw  22057  cayhamlem1  22753  caublcls  25209  ovolicc2lem4  25421  iundisj2  25450  volsup  25457  uniioombllem3  25486  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  elqaalem2  26228  aalioulem1  26240  aalioulem4  26243  aalioulem5  26244  aalioulem6  26245  aaliou  26246  aaliou3lem1  26250  aaliou3lem2  26251  aaliou3lem3  26252  aaliou3lem8  26253  aaliou3lem5  26255  aaliou3lem6  26256  aaliou3lem7  26257  taylthlem2  26282  taylthlem2OLD  26283  cxpeq  26667  zrtelqelz  26668  amgmlem  26900  lgamgulmlem4  26942  lgamcvg2  26965  wilthlem2  26979  wilth  26981  wilthimp  26982  ftalem5  26987  basellem2  26992  basellem3  26993  basellem4  26994  basellem5  26995  muval1  27043  dvdssqf  27048  sgmnncl  27057  efchtdvds  27069  mumullem2  27090  mumul  27091  sqff1o  27092  fsumdvdsdiaglem  27093  dvdsppwf1o  27096  dvdsflf1o  27097  muinv  27103  mpodvdsmulf1o  27104  dvdsmulf1o  27106  chtublem  27122  fsumvma2  27125  vmasum  27127  chpchtsum  27130  logfacubnd  27132  mersenne  27138  perfect1  27139  perfectlem1  27140  perfectlem2  27141  perfect  27142  dchrelbas4  27154  dchrfi  27166  bcmono  27188  bcp1ctr  27190  bclbnd  27191  bposlem1  27195  bposlem3  27197  bposlem5  27199  bposlem6  27200  bposlem9  27203  lgsmod  27234  lgsdir  27243  lgsdilem2  27244  lgsne0  27246  lgsqrlem2  27258  lgsqr  27262  lgsqrmodndvds  27264  gausslemma2dlem0c  27269  gausslemma2dlem0h  27274  gausslemma2dlem0i  27275  gausslemma2dlem2  27278  gausslemma2dlem6  27283  gausslemma2dlem7  27284  gausslemma2d  27285  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgseisenlem4  27289  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  lgsquad2lem1  27295  lgsquad2lem2  27296  lgsquad2  27297  m1lgs  27299  2lgslem2  27306  2sqlem3  27331  2sqlem4  27332  2sqlem8  27337  chebbnd1lem1  27380  rplogsumlem2  27396  rpvmasumlem  27398  dchrisumlem1  27400  dchrisumlem2  27401  dchrisumlem3  27402  dchrisum0fmul  27417  dchrisum0ff  27418  dchrisum0flblem1  27419  dchrisum0flblem2  27420  dchrisum0flb  27421  dchrisum0  27431  pntrsumbnd2  27478  pntrlog2bndlem1  27488  pntrlog2bndlem6  27494  pntpbnd2  27498  pntlemg  27509  pntlemj  27514  pntlemf  27516  ostth2lem2  27545  ostth2lem3  27546  ostth3  27549  numclwlk2lem2f1o  30308  nrt2irr  30402  minvecolem4  30809  iundisj2f  32519  ssnnssfz  32710  iundisj2fi  32720  f1ocnt  32725  elq2  32736  numdenneg  32739  expgt0b  32741  ltesubnnd  32747  oexpled  32772  psgnfzto1stlem  33057  isarchi3  33141  archiabllem1b  33146  zringfrac  33525  fldextrspundgdvds  33676  cos9thpiminplylem2  33773  smatrcl  33786  1smat1  33794  submateqlem1  33797  lmatfvlem  33805  qqhval2  33972  qqhf  33976  qqhghm  33978  qqhrhm  33979  qqhnm  33980  qqhre  34010  esumcvg  34076  meascnbl  34209  omssubadd  34291  oddpwdc  34345  ballotlemfp1  34483  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemimin  34497  ballotlemic  34498  ballotlem1c  34499  hgt750lemc  34638  hgt750lemd  34639  hgt750lemb  34647  hgt750leme  34649  subfaclim  35175  cvmliftlem7  35278  sinccvglem  35659  bcprod  35725  bccolsum  35726  faclimlem2  35731  faclim2  35735  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem6  37620  poimirlem8  37622  poimirlem9  37623  poimirlem10  37624  poimirlem11  37625  poimirlem13  37627  poimirlem14  37628  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem23  37637  poimirlem24  37638  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  poimirlem31  37645  mblfinlem2  37652  seqpo  37741  incsequz  37742  incsequz2  37743  zndvdchrrhm  41960  bccl2d  41979  nnproddivdvdsd  41988  lcmineqlem1  42017  lcmineqlem3  42019  lcmineqlem4  42020  lcmineqlem6  42022  lcmineqlem8  42024  lcmineqlem9  42025  lcmineqlem10  42026  lcmineqlem11  42027  lcmineqlem13  42029  lcmineqlem14  42030  lcmineqlem18  42034  lcmineqlem19  42035  lcmineqlem20  42036  lcmineqlem21  42037  lcmineqlem22  42038  lcmineqlem23  42039  lcmineqlem  42040  3lexlogpow5ineq2  42043  3lexlogpow2ineq1  42046  aks4d1p3  42066  aks4d1p5  42068  aks4d1p6  42069  aks4d1p8d1  42072  aks4d1p8d2  42073  aks4d1p8d3  42074  aks4d1p8  42075  aks4d1p9  42076  posbezout  42088  primrootscoprbij  42090  remexz  42092  primrootspoweq0  42094  aks6d1c1  42104  aks6d1c2p2  42107  hashscontpow1  42109  hashscontpow  42110  aks6d1c3  42111  aks6d1c4  42112  aks6d1c2lem4  42115  aks6d1c2  42118  aks6d1c5lem1  42124  sticksstones6  42139  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  aks6d1c6lem3  42160  aks6d1c6lem4  42161  aks6d1c6isolem3  42164  aks6d1c6lem5  42165  aks6d1c7lem2  42169  aks6d1c7  42172  aks5lem1  42174  aks5lem2  42175  aks5lem3a  42177  grpods  42182  unitscyglem1  42183  unitscyglem2  42184  unitscyglem4  42186  unitscyglem5  42187  aks5  42192  sumcubes  42301  oexpreposd  42310  explt1d  42311  expeq1d  42312  expeqidd  42313  exp11d  42314  gcdle1d  42318  gcdle2d  42319  dvdsexpnn0  42322  fimgmcyc  42522  fltdvdsabdvdsc  42626  fltaccoprm  42628  fltbccoprm  42629  fltabcoprm  42630  fltne  42632  flt4lem2  42635  flt4lem3  42636  flt4lem4  42637  flt4lem5  42638  flt4lem5elem  42639  flt4lem5a  42640  flt4lem5b  42641  flt4lem5c  42642  flt4lem5d  42643  flt4lem5e  42644  flt4lem5f  42645  flt4lem6  42646  flt4lem7  42647  nna4b4nsq  42648  fltltc  42649  fltnlta  42651  irrapxlem3  42812  irrapxlem5  42814  pellexlem5  42821  pellexlem6  42822  pellex  42823  pell1234qrmulcl  42843  jm2.23  42985  jm2.20nn  42986  jm2.26lem3  42990  jm2.27a  42994  jm2.27b  42995  jm2.27c  42996  jm3.1lem1  43006  jm3.1lem3  43008  inductionexd  44144  nznngen  44305  hashnzfz2  44310  fmuldfeq  45581  divcnvg  45625  stoweidlem1  45999  stoweidlem3  46001  stoweidlem11  46009  stoweidlem20  46018  stoweidlem26  46024  stoweidlem34  46032  stoweidlem51  46049  stirlinglem4  46075  stirlinglem5  46076  stirlinglem8  46079  dirkerper  46094  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  dirkercncflem2  46102  fourierdlem11  46116  fourierdlem14  46119  fourierdlem20  46125  fourierdlem25  46130  fourierdlem37  46142  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  fourierdlem54  46158  fourierdlem64  46168  fourierdlem73  46177  fourierdlem79  46183  fourierdlem92  46196  fourierdlem93  46197  fourierdlem111  46215  sqwvfourb  46227  etransclem3  46235  etransclem7  46239  etransclem10  46242  etransclem15  46247  etransclem24  46256  etransclem25  46257  etransclem26  46258  etransclem27  46259  etransclem28  46260  etransclem35  46267  etransclem37  46269  etransclem38  46270  etransclem41  46273  etransclem44  46276  etransclem45  46277  etransclem48  46280  ovnsubaddlem1  46568  vonioolem1  46678  iccpartgtprec  47421  iccpartipre  47422  fmtnoodd  47534  goldbachthlem2  47547  goldbachth  47548  odz2prm2pw  47564  fmtnoprmfac1lem  47565  fmtnoprmfac2lem1  47567  fmtnoprmfac2  47568  fmtnofac2lem  47569  2pwp1prm  47590  lighneallem1  47606  lighneallem4  47611  proththdlem  47614  proththd  47615  divgcdoddALTV  47683  perfectALTVlem1  47722  perfectALTVlem2  47723  perfectALTV  47724  gbowge7  47764  gpgedgvtx1  48053  gpg3kgrtriexlem2  48075  gpg3kgrtriexlem5  48078  pw2m1lepw2m1  48509  nnolog2flm1  48579  dignn0fr  48590  dignn0flhalflem1  48604