Theorem nnzd 12637

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℕcn 12263  ℤcz 12610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-neg 11492  df-nn 12264  df-n0 12524  df-z 12611

This theorem is referenced by:  expaddzlem  14142  expmulz  14145  expmulnbnd  14270  facndiv  14323  bcval5  14353  bcpasc  14356  hashf1  14492  isercolllem1  15697  isercolllem2  15698  o1fsum  15845  bcxmas  15867  climcndslem2  15882  climcnds  15883  mertenslem1  15916  fprodser  15981  bpolydiflem  16086  eftlub  16141  eirrlem  16236  rpnnen2lem7  16252  rpnnen2lem9  16254  rpnnen2lem11  16256  sqrt2irrlem  16280  dvdsfac  16359  dvdsmod  16362  oddpwp1fsum  16425  bitsfzolem  16467  bitsmod  16469  bitsfi  16470  bitscmp  16471  bitsinv1  16475  sadadd3  16494  sadaddlem  16499  bitsuz  16507  bitsshft  16508  gcdnncl  16540  gcd1  16561  dvdsgcdidd  16570  bezoutlem3  16574  bezoutlem4  16575  mulgcd  16581  rplpwr  16591  rprpwr  16592  sqgcd  16595  expgcd  16596  nn0expgcd  16597  dvdssq  16600  lcmneg  16636  lcmgcdlem  16639  rpdvds  16693  coprmprod  16694  coprmproddvdslem  16695  congr  16697  cncongr1  16700  cncongr2  16701  prmz  16708  prmind2  16718  divgcdodd  16743  isprm6  16747  prmexpb  16752  prmfac1  16753  rpexp  16755  prmdvdsbc  16759  prmdvdsncoprmbd  16760  numdensq  16787  numdenexp  16793  hashdvds  16808  phiprmpw  16809  crth  16811  phimullem  16812  eulerthlem1  16814  eulerthlem2  16815  prmdivdiv  16820  hashgcdlem  16821  odzdvds  16828  pythagtriplem4  16852  pythagtriplem6  16854  pythagtriplem7  16855  pythagtriplem11  16858  pythagtriplem13  16860  pythagtriplem19  16866  pclem  16871  pcprendvds2  16874  pcpre1  16875  pcpremul  16876  pceulem  16878  pcqmul  16886  pcdvdsb  16902  pcidlem  16905  pcdvdstr  16909  pcgcd1  16910  pc2dvds  16912  pcprmpw2  16915  pcaddlem  16921  pcadd  16922  pcmpt2  16926  pcmptdvds  16927  pcfac  16932  pcbc  16933  qexpz  16934  oddprmdvds  16936  prmpwdvds  16937  pockthlem  16938  pockthg  16939  prmreclem2  16950  prmreclem3  16951  prmreclem4  16952  prmreclem5  16953  prmreclem6  16954  4sqlem5  16975  4sqlem8  16978  4sqlem9  16979  4sqlem10  16980  4sqlem12  16989  4sqlem14  16991  4sqlem16  16993  4sqlem17  16994  vdwlem1  17014  vdwlem2  17015  vdwlem3  17016  vdwlem6  17019  vdwlem9  17022  vdwlem10  17023  vdwnnlem3  17030  prmdvdsprmop  17076  prmolelcmf  17081  prmgaplem1  17082  prmgaplem7  17090  prmgaplem8  17091  gsumwsubmcl  18862  gsumsgrpccat  18865  gsumwmhm  18870  mulgneg  19122  mulgnndir  19133  psgnunilem4  19529  odlem2  19571  mndodconglem  19573  odmod  19578  gexlem2  19614  gexcl3  19619  gexcl2  19621  sylow1lem1  19630  sylow1lem3  19632  sylow1lem5  19634  pgpfi  19637  fislw  19657  sylow3lem4  19662  gexexlem  19884  ablfacrplem  20099  ablfacrp  20100  ablfacrp2  20101  ablfac1lem  20102  ablfac1b  20104  ablfac1eu  20107  pgpfac1lem3a  20110  ablfaclem3  20121  fincygsubgd  20145  fincygsubgodd  20146  znrrg  21601  cayhamlem1  22887  caublcls  25356  ovolicc2lem4  25568  iundisj2  25597  volsup  25604  uniioombllem3  25633  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  elqaalem2  26376  aalioulem1  26388  aalioulem4  26391  aalioulem5  26392  aalioulem6  26393  aaliou  26394  aaliou3lem1  26398  aaliou3lem2  26399  aaliou3lem3  26400  aaliou3lem8  26401  aaliou3lem5  26403  aaliou3lem6  26404  aaliou3lem7  26405  taylthlem2  26430  taylthlem2OLD  26431  cxpeq  26814  zrtelqelz  26815  amgmlem  27047  lgamgulmlem4  27089  lgamcvg2  27112  wilthlem2  27126  wilth  27128  wilthimp  27129  ftalem5  27134  basellem2  27139  basellem3  27140  basellem4  27141  basellem5  27142  muval1  27190  dvdssqf  27195  sgmnncl  27204  efchtdvds  27216  mumullem2  27237  mumul  27238  sqff1o  27239  fsumdvdsdiaglem  27240  dvdsppwf1o  27243  dvdsflf1o  27244  muinv  27250  mpodvdsmulf1o  27251  dvdsmulf1o  27253  chtublem  27269  fsumvma2  27272  vmasum  27274  chpchtsum  27277  logfacubnd  27279  mersenne  27285  perfect1  27286  perfectlem1  27287  perfectlem2  27288  perfect  27289  dchrelbas4  27301  dchrfi  27313  bcmono  27335  bcp1ctr  27337  bclbnd  27338  bposlem1  27342  bposlem3  27344  bposlem5  27346  bposlem6  27347  bposlem9  27350  lgsmod  27381  lgsdir  27390  lgsdilem2  27391  lgsne0  27393  lgsqrlem2  27405  lgsqr  27409  lgsqrmodndvds  27411  gausslemma2dlem0c  27416  gausslemma2dlem0h  27421  gausslemma2dlem0i  27422  gausslemma2dlem2  27425  gausslemma2dlem6  27430  gausslemma2dlem7  27431  gausslemma2d  27432  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem3  27435  lgseisenlem4  27436  lgsquadlem1  27438  lgsquadlem2  27439  lgsquadlem3  27440  lgsquad2lem1  27442  lgsquad2lem2  27443  lgsquad2  27444  m1lgs  27446  2lgslem2  27453  2sqlem3  27478  2sqlem4  27479  2sqlem8  27484  chebbnd1lem1  27527  rplogsumlem2  27543  rpvmasumlem  27545  dchrisumlem1  27547  dchrisumlem2  27548  dchrisumlem3  27549  dchrisum0fmul  27564  dchrisum0ff  27565  dchrisum0flblem1  27566  dchrisum0flblem2  27567  dchrisum0flb  27568  dchrisum0  27578  pntrsumbnd2  27625  pntrlog2bndlem1  27635  pntrlog2bndlem6  27641  pntpbnd2  27645  pntlemg  27656  pntlemj  27661  pntlemf  27663  ostth2lem2  27692  ostth2lem3  27693  ostth3  27696  numclwlk2lem2f1o  30407  nrt2irr  30501  minvecolem4  30908  iundisj2f  32609  ssnnssfz  32795  iundisj2fi  32804  f1ocnt  32809  numdenneg  32820  expgt0b  32822  ltesubnnd  32828  psgnfzto1stlem  33102  isarchi3  33176  archiabllem1b  33181  zringfrac  33561  smatrcl  33756  1smat1  33764  submateqlem1  33767  lmatfvlem  33775  qqhval2  33944  qqhf  33948  qqhghm  33950  qqhrhm  33951  qqhnm  33952  qqhre  33982  esumcvg  34066  meascnbl  34199  omssubadd  34281  oddpwdc  34335  ballotlemfp1  34472  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemimin  34486  ballotlemic  34487  ballotlem1c  34488  hgt750lemc  34640  hgt750lemd  34641  hgt750lemb  34649  hgt750leme  34651  subfaclim  35172  cvmliftlem7  35275  sinccvglem  35656  bcprod  35717  bccolsum  35718  faclimlem2  35723  faclim2  35727  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem4  37610  poimirlem6  37612  poimirlem8  37614  poimirlem9  37615  poimirlem10  37616  poimirlem11  37617  poimirlem13  37619  poimirlem14  37620  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem26  37632  poimirlem27  37633  poimirlem28  37634  poimirlem31  37637  mblfinlem2  37644  seqpo  37733  incsequz  37734  incsequz2  37735  zndvdchrrhm  41952  bccl2d  41972  nnproddivdvdsd  41981  lcmineqlem1  42010  lcmineqlem3  42012  lcmineqlem4  42013  lcmineqlem6  42015  lcmineqlem8  42017  lcmineqlem9  42018  lcmineqlem10  42019  lcmineqlem11  42020  lcmineqlem13  42022  lcmineqlem14  42023  lcmineqlem18  42027  lcmineqlem19  42028  lcmineqlem20  42029  lcmineqlem21  42030  lcmineqlem22  42031  lcmineqlem23  42032  lcmineqlem  42033  3lexlogpow5ineq2  42036  3lexlogpow2ineq1  42039  aks4d1p3  42059  aks4d1p5  42061  aks4d1p6  42062  aks4d1p8d1  42065  aks4d1p8d2  42066  aks4d1p8d3  42067  aks4d1p8  42068  aks4d1p9  42069  posbezout  42081  primrootscoprbij  42083  remexz  42085  primrootspoweq0  42087  aks6d1c1  42097  aks6d1c2p2  42100  hashscontpow1  42102  hashscontpow  42103  aks6d1c3  42104  aks6d1c4  42105  aks6d1c2lem4  42108  aks6d1c2  42111  aks6d1c5lem1  42117  sticksstones6  42132  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  aks6d1c6lem3  42153  aks6d1c6lem4  42154  aks6d1c6isolem3  42157  aks6d1c6lem5  42158  aks6d1c7lem2  42162  aks6d1c7  42165  aks5lem1  42167  aks5lem2  42168  aks5lem3a  42170  grpods  42175  unitscyglem1  42176  unitscyglem2  42177  unitscyglem4  42179  unitscyglem5  42180  aks5  42185  metakunt1  42186  metakunt2  42187  metakunt3  42188  metakunt4  42189  metakunt5  42190  metakunt7  42192  metakunt10  42195  metakunt15  42200  metakunt16  42201  metakunt18  42203  metakunt19  42204  metakunt20  42205  metakunt21  42206  metakunt22  42207  metakunt24  42209  metakunt25  42210  metakunt26  42211  metakunt27  42212  metakunt28  42213  metakunt29  42214  metakunt30  42215  metakunt32  42217  metakunt33  42218  sumcubes  42325  oexpreposd  42335  explt1d  42336  expeq1d  42337  expeqidd  42338  exp11d  42339  gcdle1d  42343  gcdle2d  42344  dvdsexpnn0  42347  fimgmcyc  42520  fltdvdsabdvdsc  42624  fltaccoprm  42626  fltbccoprm  42627  fltabcoprm  42628  fltne  42630  flt4lem2  42633  flt4lem3  42634  flt4lem4  42635  flt4lem5  42636  flt4lem5elem  42637  flt4lem5a  42638  flt4lem5b  42639  flt4lem5c  42640  flt4lem5d  42641  flt4lem5e  42642  flt4lem5f  42643  flt4lem6  42644  flt4lem7  42645  nna4b4nsq  42646  fltltc  42647  fltnlta  42649  irrapxlem3  42811  irrapxlem5  42813  pellexlem5  42820  pellexlem6  42821  pellex  42822  pell1234qrmulcl  42842  jm2.23  42984  jm2.20nn  42985  jm2.26lem3  42989  jm2.27a  42993  jm2.27b  42994  jm2.27c  42995  jm3.1lem1  43005  jm3.1lem3  43007  inductionexd  44144  nznngen  44311  hashnzfz2  44316  fmuldfeq  45538  divcnvg  45582  stoweidlem1  45956  stoweidlem3  45958  stoweidlem11  45966  stoweidlem20  45975  stoweidlem26  45981  stoweidlem34  45989  stoweidlem51  46006  stirlinglem4  46032  stirlinglem5  46033  stirlinglem8  46036  dirkerper  46051  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  dirkercncflem2  46059  fourierdlem11  46073  fourierdlem14  46076  fourierdlem20  46082  fourierdlem25  46087  fourierdlem37  46099  fourierdlem41  46103  fourierdlem48  46109  fourierdlem49  46110  fourierdlem54  46115  fourierdlem64  46125  fourierdlem73  46134  fourierdlem79  46140  fourierdlem92  46153  fourierdlem93  46154  fourierdlem111  46172  sqwvfourb  46184  etransclem3  46192  etransclem7  46196  etransclem10  46199  etransclem15  46204  etransclem24  46213  etransclem25  46214  etransclem26  46215  etransclem27  46216  etransclem28  46217  etransclem35  46224  etransclem37  46226  etransclem38  46227  etransclem41  46230  etransclem44  46233  etransclem45  46234  etransclem48  46237  ovnsubaddlem1  46525  vonioolem1  46635  iccpartgtprec  47344  iccpartipre  47345  fmtnoodd  47457  goldbachthlem2  47470  goldbachth  47471  odz2prm2pw  47487  fmtnoprmfac1lem  47488  fmtnoprmfac2lem1  47490  fmtnoprmfac2  47491  fmtnofac2lem  47492  2pwp1prm  47513  lighneallem1  47529  lighneallem4  47534  proththdlem  47537  proththd  47538  divgcdoddALTV  47606  perfectALTVlem1  47645  perfectALTVlem2  47646  perfectALTV  47647  gbowge7  47687  gpgedgvtx1  47954  pw2m1lepw2m1  48365  nnolog2flm1  48439  dignn0fr  48450  dignn0flhalflem1  48464