Theorem nnzd 12563

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℕcn 12193  ℤcz 12536

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-neg 11415  df-nn 12194  df-n0 12450  df-z 12537

This theorem is referenced by:  expaddzlem  14077  expmulz  14080  expmulnbnd  14207  facndiv  14260  bcval5  14290  bcpasc  14293  hashf1  14429  isercolllem1  15638  isercolllem2  15639  o1fsum  15786  bcxmas  15808  climcndslem2  15823  climcnds  15824  mertenslem1  15857  fprodser  15922  bpolydiflem  16027  eftlub  16084  eirrlem  16179  rpnnen2lem7  16195  rpnnen2lem9  16197  rpnnen2lem11  16199  sqrt2irrlem  16223  dvdsfac  16303  dvdsmod  16306  oddpwp1fsum  16369  bitsfzolem  16411  bitsmod  16413  bitsfi  16414  bitscmp  16415  bitsinv1  16419  sadadd3  16438  sadaddlem  16443  bitsuz  16451  bitsshft  16452  gcdnncl  16484  gcd1  16505  dvdsgcdidd  16514  bezoutlem3  16518  bezoutlem4  16519  mulgcd  16525  rplpwr  16535  rprpwr  16536  sqgcd  16539  expgcd  16540  nn0expgcd  16541  dvdssq  16544  lcmneg  16580  lcmgcdlem  16583  rpdvds  16637  coprmprod  16638  coprmproddvdslem  16639  congr  16641  cncongr1  16644  cncongr2  16645  prmz  16652  prmind2  16662  divgcdodd  16687  isprm6  16691  prmexpb  16696  prmfac1  16697  rpexp  16699  prmdvdsbc  16703  prmdvdsncoprmbd  16704  numdensq  16731  numdenexp  16737  hashdvds  16752  phiprmpw  16753  crth  16755  phimullem  16756  eulerthlem1  16758  eulerthlem2  16759  prmdivdiv  16764  hashgcdlem  16765  odzdvds  16773  pythagtriplem4  16797  pythagtriplem6  16799  pythagtriplem7  16800  pythagtriplem11  16803  pythagtriplem13  16805  pythagtriplem19  16811  pclem  16816  pcprendvds2  16819  pcpre1  16820  pcpremul  16821  pceulem  16823  pcqmul  16831  pcdvdsb  16847  pcidlem  16850  pcdvdstr  16854  pcgcd1  16855  pc2dvds  16857  pcprmpw2  16860  pcaddlem  16866  pcadd  16867  pcmpt2  16871  pcmptdvds  16872  pcfac  16877  pcbc  16878  qexpz  16879  oddprmdvds  16881  prmpwdvds  16882  pockthlem  16883  pockthg  16884  prmreclem2  16895  prmreclem3  16896  prmreclem4  16897  prmreclem5  16898  prmreclem6  16899  4sqlem5  16920  4sqlem8  16923  4sqlem9  16924  4sqlem10  16925  4sqlem12  16934  4sqlem14  16936  4sqlem16  16938  4sqlem17  16939  vdwlem1  16959  vdwlem2  16960  vdwlem3  16961  vdwlem6  16964  vdwlem9  16967  vdwlem10  16968  vdwnnlem3  16975  prmdvdsprmop  17021  prmolelcmf  17026  prmgaplem1  17027  prmgaplem7  17035  prmgaplem8  17036  gsumwsubmcl  18771  gsumsgrpccat  18774  gsumwmhm  18779  mulgneg  19031  mulgnndir  19042  psgnunilem4  19434  odlem2  19476  mndodconglem  19478  odmod  19483  gexlem2  19519  gexcl3  19524  gexcl2  19526  sylow1lem1  19535  sylow1lem3  19537  sylow1lem5  19539  pgpfi  19542  fislw  19562  sylow3lem4  19567  gexexlem  19789  ablfacrplem  20004  ablfacrp  20005  ablfacrp2  20006  ablfac1lem  20007  ablfac1b  20009  ablfac1eu  20012  pgpfac1lem3a  20015  ablfaclem3  20026  fincygsubgd  20050  fincygsubgodd  20051  znrrg  21482  psdpw  22064  cayhamlem1  22760  caublcls  25216  ovolicc2lem4  25428  iundisj2  25457  volsup  25464  uniioombllem3  25493  mbfi1fseqlem3  25625  mbfi1fseqlem4  25626  elqaalem2  26235  aalioulem1  26247  aalioulem4  26250  aalioulem5  26251  aalioulem6  26252  aaliou  26253  aaliou3lem1  26257  aaliou3lem2  26258  aaliou3lem3  26259  aaliou3lem8  26260  aaliou3lem5  26262  aaliou3lem6  26263  aaliou3lem7  26264  taylthlem2  26289  taylthlem2OLD  26290  cxpeq  26674  zrtelqelz  26675  amgmlem  26907  lgamgulmlem4  26949  lgamcvg2  26972  wilthlem2  26986  wilth  26988  wilthimp  26989  ftalem5  26994  basellem2  26999  basellem3  27000  basellem4  27001  basellem5  27002  muval1  27050  dvdssqf  27055  sgmnncl  27064  efchtdvds  27076  mumullem2  27097  mumul  27098  sqff1o  27099  fsumdvdsdiaglem  27100  dvdsppwf1o  27103  dvdsflf1o  27104  muinv  27110  mpodvdsmulf1o  27111  dvdsmulf1o  27113  chtublem  27129  fsumvma2  27132  vmasum  27134  chpchtsum  27137  logfacubnd  27139  mersenne  27145  perfect1  27146  perfectlem1  27147  perfectlem2  27148  perfect  27149  dchrelbas4  27161  dchrfi  27173  bcmono  27195  bcp1ctr  27197  bclbnd  27198  bposlem1  27202  bposlem3  27204  bposlem5  27206  bposlem6  27207  bposlem9  27210  lgsmod  27241  lgsdir  27250  lgsdilem2  27251  lgsne0  27253  lgsqrlem2  27265  lgsqr  27269  lgsqrmodndvds  27271  gausslemma2dlem0c  27276  gausslemma2dlem0h  27281  gausslemma2dlem0i  27282  gausslemma2dlem2  27285  gausslemma2dlem6  27290  gausslemma2dlem7  27291  gausslemma2d  27292  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem3  27295  lgseisenlem4  27296  lgsquadlem1  27298  lgsquadlem2  27299  lgsquadlem3  27300  lgsquad2lem1  27302  lgsquad2lem2  27303  lgsquad2  27304  m1lgs  27306  2lgslem2  27313  2sqlem3  27338  2sqlem4  27339  2sqlem8  27344  chebbnd1lem1  27387  rplogsumlem2  27403  rpvmasumlem  27405  dchrisumlem1  27407  dchrisumlem2  27408  dchrisumlem3  27409  dchrisum0fmul  27424  dchrisum0ff  27425  dchrisum0flblem1  27426  dchrisum0flblem2  27427  dchrisum0flb  27428  dchrisum0  27438  pntrsumbnd2  27485  pntrlog2bndlem1  27495  pntrlog2bndlem6  27501  pntpbnd2  27505  pntlemg  27516  pntlemj  27521  pntlemf  27523  ostth2lem2  27552  ostth2lem3  27553  ostth3  27556  numclwlk2lem2f1o  30315  nrt2irr  30409  minvecolem4  30816  iundisj2f  32526  ssnnssfz  32717  iundisj2fi  32727  f1ocnt  32732  elq2  32743  numdenneg  32746  expgt0b  32748  ltesubnnd  32754  oexpled  32779  psgnfzto1stlem  33064  isarchi3  33148  archiabllem1b  33153  zringfrac  33532  fldextrspundgdvds  33683  cos9thpiminplylem2  33780  smatrcl  33793  1smat1  33801  submateqlem1  33804  lmatfvlem  33812  qqhval2  33979  qqhf  33983  qqhghm  33985  qqhrhm  33986  qqhnm  33987  qqhre  34017  esumcvg  34083  meascnbl  34216  omssubadd  34298  oddpwdc  34352  ballotlemfp1  34490  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemimin  34504  ballotlemic  34505  ballotlem1c  34506  hgt750lemc  34645  hgt750lemd  34646  hgt750lemb  34654  hgt750leme  34656  subfaclim  35182  cvmliftlem7  35285  sinccvglem  35666  bcprod  35732  bccolsum  35733  faclimlem2  35738  faclim2  35742  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem4  37625  poimirlem6  37627  poimirlem8  37629  poimirlem9  37630  poimirlem10  37631  poimirlem11  37632  poimirlem13  37634  poimirlem14  37635  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem23  37644  poimirlem24  37645  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  poimirlem31  37652  mblfinlem2  37659  seqpo  37748  incsequz  37749  incsequz2  37750  zndvdchrrhm  41967  bccl2d  41986  nnproddivdvdsd  41995  lcmineqlem1  42024  lcmineqlem3  42026  lcmineqlem4  42027  lcmineqlem6  42029  lcmineqlem8  42031  lcmineqlem9  42032  lcmineqlem10  42033  lcmineqlem11  42034  lcmineqlem13  42036  lcmineqlem14  42037  lcmineqlem18  42041  lcmineqlem19  42042  lcmineqlem20  42043  lcmineqlem21  42044  lcmineqlem22  42045  lcmineqlem23  42046  lcmineqlem  42047  3lexlogpow5ineq2  42050  3lexlogpow2ineq1  42053  aks4d1p3  42073  aks4d1p5  42075  aks4d1p6  42076  aks4d1p8d1  42079  aks4d1p8d2  42080  aks4d1p8d3  42081  aks4d1p8  42082  aks4d1p9  42083  posbezout  42095  primrootscoprbij  42097  remexz  42099  primrootspoweq0  42101  aks6d1c1  42111  aks6d1c2p2  42114  hashscontpow1  42116  hashscontpow  42117  aks6d1c3  42118  aks6d1c4  42119  aks6d1c2lem4  42122  aks6d1c2  42125  aks6d1c5lem1  42131  sticksstones6  42146  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  aks6d1c6lem3  42167  aks6d1c6lem4  42168  aks6d1c6isolem3  42171  aks6d1c6lem5  42172  aks6d1c7lem2  42176  aks6d1c7  42179  aks5lem1  42181  aks5lem2  42182  aks5lem3a  42184  grpods  42189  unitscyglem1  42190  unitscyglem2  42191  unitscyglem4  42193  unitscyglem5  42194  aks5  42199  sumcubes  42308  oexpreposd  42317  explt1d  42318  expeq1d  42319  expeqidd  42320  exp11d  42321  gcdle1d  42325  gcdle2d  42326  dvdsexpnn0  42329  fimgmcyc  42529  fltdvdsabdvdsc  42633  fltaccoprm  42635  fltbccoprm  42636  fltabcoprm  42637  fltne  42639  flt4lem2  42642  flt4lem3  42643  flt4lem4  42644  flt4lem5  42645  flt4lem5elem  42646  flt4lem5a  42647  flt4lem5b  42648  flt4lem5c  42649  flt4lem5d  42650  flt4lem5e  42651  flt4lem5f  42652  flt4lem6  42653  flt4lem7  42654  nna4b4nsq  42655  fltltc  42656  fltnlta  42658  irrapxlem3  42819  irrapxlem5  42821  pellexlem5  42828  pellexlem6  42829  pellex  42830  pell1234qrmulcl  42850  jm2.23  42992  jm2.20nn  42993  jm2.26lem3  42997  jm2.27a  43001  jm2.27b  43002  jm2.27c  43003  jm3.1lem1  43013  jm3.1lem3  43015  inductionexd  44151  nznngen  44312  hashnzfz2  44317  fmuldfeq  45588  divcnvg  45632  stoweidlem1  46006  stoweidlem3  46008  stoweidlem11  46016  stoweidlem20  46025  stoweidlem26  46031  stoweidlem34  46039  stoweidlem51  46056  stirlinglem4  46082  stirlinglem5  46083  stirlinglem8  46086  dirkerper  46101  dirkertrigeqlem2  46104  dirkertrigeqlem3  46105  dirkercncflem2  46109  fourierdlem11  46123  fourierdlem14  46126  fourierdlem20  46132  fourierdlem25  46137  fourierdlem37  46149  fourierdlem41  46153  fourierdlem48  46159  fourierdlem49  46160  fourierdlem54  46165  fourierdlem64  46175  fourierdlem73  46184  fourierdlem79  46190  fourierdlem92  46203  fourierdlem93  46204  fourierdlem111  46222  sqwvfourb  46234  etransclem3  46242  etransclem7  46246  etransclem10  46249  etransclem15  46254  etransclem24  46263  etransclem25  46264  etransclem26  46265  etransclem27  46266  etransclem28  46267  etransclem35  46274  etransclem37  46276  etransclem38  46277  etransclem41  46280  etransclem44  46283  etransclem45  46284  etransclem48  46287  ovnsubaddlem1  46575  vonioolem1  46685  iccpartgtprec  47425  iccpartipre  47426  fmtnoodd  47538  goldbachthlem2  47551  goldbachth  47552  odz2prm2pw  47568  fmtnoprmfac1lem  47569  fmtnoprmfac2lem1  47571  fmtnoprmfac2  47572  fmtnofac2lem  47573  2pwp1prm  47594  lighneallem1  47610  lighneallem4  47615  proththdlem  47618  proththd  47619  divgcdoddALTV  47687  perfectALTVlem1  47726  perfectALTVlem2  47727  perfectALTV  47728  gbowge7  47768  gpgedgvtx1  48057  gpg3kgrtriexlem2  48079  gpg3kgrtriexlem5  48082  pw2m1lepw2m1  48513  nnolog2flm1  48583  dignn0fr  48594  dignn0flhalflem1  48608