Theorem nnzd 12640

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℕcn 12266  ℤcz 12613

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-neg 11495  df-nn 12267  df-n0 12527  df-z 12614

This theorem is referenced by:  expaddzlem  14146  expmulz  14149  expmulnbnd  14274  facndiv  14327  bcval5  14357  bcpasc  14360  hashf1  14496  isercolllem1  15701  isercolllem2  15702  o1fsum  15849  bcxmas  15871  climcndslem2  15886  climcnds  15887  mertenslem1  15920  fprodser  15985  bpolydiflem  16090  eftlub  16145  eirrlem  16240  rpnnen2lem7  16256  rpnnen2lem9  16258  rpnnen2lem11  16260  sqrt2irrlem  16284  dvdsfac  16363  dvdsmod  16366  oddpwp1fsum  16429  bitsfzolem  16471  bitsmod  16473  bitsfi  16474  bitscmp  16475  bitsinv1  16479  sadadd3  16498  sadaddlem  16503  bitsuz  16511  bitsshft  16512  gcdnncl  16544  gcd1  16565  dvdsgcdidd  16574  bezoutlem3  16578  bezoutlem4  16579  mulgcd  16585  rplpwr  16595  rprpwr  16596  sqgcd  16599  expgcd  16600  nn0expgcd  16601  dvdssq  16604  lcmneg  16640  lcmgcdlem  16643  rpdvds  16697  coprmprod  16698  coprmproddvdslem  16699  congr  16701  cncongr1  16704  cncongr2  16705  prmz  16712  prmind2  16722  divgcdodd  16747  isprm6  16751  prmexpb  16756  prmfac1  16757  rpexp  16759  prmdvdsbc  16763  prmdvdsncoprmbd  16764  numdensq  16791  numdenexp  16797  hashdvds  16812  phiprmpw  16813  crth  16815  phimullem  16816  eulerthlem1  16818  eulerthlem2  16819  prmdivdiv  16824  hashgcdlem  16825  odzdvds  16833  pythagtriplem4  16857  pythagtriplem6  16859  pythagtriplem7  16860  pythagtriplem11  16863  pythagtriplem13  16865  pythagtriplem19  16871  pclem  16876  pcprendvds2  16879  pcpre1  16880  pcpremul  16881  pceulem  16883  pcqmul  16891  pcdvdsb  16907  pcidlem  16910  pcdvdstr  16914  pcgcd1  16915  pc2dvds  16917  pcprmpw2  16920  pcaddlem  16926  pcadd  16927  pcmpt2  16931  pcmptdvds  16932  pcfac  16937  pcbc  16938  qexpz  16939  oddprmdvds  16941  prmpwdvds  16942  pockthlem  16943  pockthg  16944  prmreclem2  16955  prmreclem3  16956  prmreclem4  16957  prmreclem5  16958  prmreclem6  16959  4sqlem5  16980  4sqlem8  16983  4sqlem9  16984  4sqlem10  16985  4sqlem12  16994  4sqlem14  16996  4sqlem16  16998  4sqlem17  16999  vdwlem1  17019  vdwlem2  17020  vdwlem3  17021  vdwlem6  17024  vdwlem9  17027  vdwlem10  17028  vdwnnlem3  17035  prmdvdsprmop  17081  prmolelcmf  17086  prmgaplem1  17087  prmgaplem7  17095  prmgaplem8  17096  gsumwsubmcl  18850  gsumsgrpccat  18853  gsumwmhm  18858  mulgneg  19110  mulgnndir  19121  psgnunilem4  19515  odlem2  19557  mndodconglem  19559  odmod  19564  gexlem2  19600  gexcl3  19605  gexcl2  19607  sylow1lem1  19616  sylow1lem3  19618  sylow1lem5  19620  pgpfi  19623  fislw  19643  sylow3lem4  19648  gexexlem  19870  ablfacrplem  20085  ablfacrp  20086  ablfacrp2  20087  ablfac1lem  20088  ablfac1b  20090  ablfac1eu  20093  pgpfac1lem3a  20096  ablfaclem3  20107  fincygsubgd  20131  fincygsubgodd  20132  znrrg  21584  psdpw  22174  cayhamlem1  22872  caublcls  25343  ovolicc2lem4  25555  iundisj2  25584  volsup  25591  uniioombllem3  25620  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  elqaalem2  26362  aalioulem1  26374  aalioulem4  26377  aalioulem5  26378  aalioulem6  26379  aaliou  26380  aaliou3lem1  26384  aaliou3lem2  26385  aaliou3lem3  26386  aaliou3lem8  26387  aaliou3lem5  26389  aaliou3lem6  26390  aaliou3lem7  26391  taylthlem2  26416  taylthlem2OLD  26417  cxpeq  26800  zrtelqelz  26801  amgmlem  27033  lgamgulmlem4  27075  lgamcvg2  27098  wilthlem2  27112  wilth  27114  wilthimp  27115  ftalem5  27120  basellem2  27125  basellem3  27126  basellem4  27127  basellem5  27128  muval1  27176  dvdssqf  27181  sgmnncl  27190  efchtdvds  27202  mumullem2  27223  mumul  27224  sqff1o  27225  fsumdvdsdiaglem  27226  dvdsppwf1o  27229  dvdsflf1o  27230  muinv  27236  mpodvdsmulf1o  27237  dvdsmulf1o  27239  chtublem  27255  fsumvma2  27258  vmasum  27260  chpchtsum  27263  logfacubnd  27265  mersenne  27271  perfect1  27272  perfectlem1  27273  perfectlem2  27274  perfect  27275  dchrelbas4  27287  dchrfi  27299  bcmono  27321  bcp1ctr  27323  bclbnd  27324  bposlem1  27328  bposlem3  27330  bposlem5  27332  bposlem6  27333  bposlem9  27336  lgsmod  27367  lgsdir  27376  lgsdilem2  27377  lgsne0  27379  lgsqrlem2  27391  lgsqr  27395  lgsqrmodndvds  27397  gausslemma2dlem0c  27402  gausslemma2dlem0h  27407  gausslemma2dlem0i  27408  gausslemma2dlem2  27411  gausslemma2dlem6  27416  gausslemma2dlem7  27417  gausslemma2d  27418  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem3  27421  lgseisenlem4  27422  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  lgsquad2lem1  27428  lgsquad2lem2  27429  lgsquad2  27430  m1lgs  27432  2lgslem2  27439  2sqlem3  27464  2sqlem4  27465  2sqlem8  27470  chebbnd1lem1  27513  rplogsumlem2  27529  rpvmasumlem  27531  dchrisumlem1  27533  dchrisumlem2  27534  dchrisumlem3  27535  dchrisum0fmul  27550  dchrisum0ff  27551  dchrisum0flblem1  27552  dchrisum0flblem2  27553  dchrisum0flb  27554  dchrisum0  27564  pntrsumbnd2  27611  pntrlog2bndlem1  27621  pntrlog2bndlem6  27627  pntpbnd2  27631  pntlemg  27642  pntlemj  27647  pntlemf  27649  ostth2lem2  27678  ostth2lem3  27679  ostth3  27682  numclwlk2lem2f1o  30398  nrt2irr  30492  minvecolem4  30899  iundisj2f  32603  ssnnssfz  32789  iundisj2fi  32799  f1ocnt  32804  numdenneg  32816  expgt0b  32818  ltesubnnd  32824  psgnfzto1stlem  33120  isarchi3  33194  archiabllem1b  33199  zringfrac  33582  fldextrspundgdvds  33731  smatrcl  33795  1smat1  33803  submateqlem1  33806  lmatfvlem  33814  qqhval2  33983  qqhf  33987  qqhghm  33989  qqhrhm  33990  qqhnm  33991  qqhre  34021  esumcvg  34087  meascnbl  34220  omssubadd  34302  oddpwdc  34356  ballotlemfp1  34494  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemimin  34508  ballotlemic  34509  ballotlem1c  34510  hgt750lemc  34662  hgt750lemd  34663  hgt750lemb  34671  hgt750leme  34673  subfaclim  35193  cvmliftlem7  35296  sinccvglem  35677  bcprod  35738  bccolsum  35739  faclimlem2  35744  faclim2  35748  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem4  37631  poimirlem6  37633  poimirlem8  37635  poimirlem9  37636  poimirlem10  37637  poimirlem11  37638  poimirlem13  37640  poimirlem14  37641  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  poimirlem31  37658  mblfinlem2  37665  seqpo  37754  incsequz  37755  incsequz2  37756  zndvdchrrhm  41972  bccl2d  41992  nnproddivdvdsd  42001  lcmineqlem1  42030  lcmineqlem3  42032  lcmineqlem4  42033  lcmineqlem6  42035  lcmineqlem8  42037  lcmineqlem9  42038  lcmineqlem10  42039  lcmineqlem11  42040  lcmineqlem13  42042  lcmineqlem14  42043  lcmineqlem18  42047  lcmineqlem19  42048  lcmineqlem20  42049  lcmineqlem21  42050  lcmineqlem22  42051  lcmineqlem23  42052  lcmineqlem  42053  3lexlogpow5ineq2  42056  3lexlogpow2ineq1  42059  aks4d1p3  42079  aks4d1p5  42081  aks4d1p6  42082  aks4d1p8d1  42085  aks4d1p8d2  42086  aks4d1p8d3  42087  aks4d1p8  42088  aks4d1p9  42089  posbezout  42101  primrootscoprbij  42103  remexz  42105  primrootspoweq0  42107  aks6d1c1  42117  aks6d1c2p2  42120  hashscontpow1  42122  hashscontpow  42123  aks6d1c3  42124  aks6d1c4  42125  aks6d1c2lem4  42128  aks6d1c2  42131  aks6d1c5lem1  42137  sticksstones6  42152  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  aks6d1c6lem3  42173  aks6d1c6lem4  42174  aks6d1c6isolem3  42177  aks6d1c6lem5  42178  aks6d1c7lem2  42182  aks6d1c7  42185  aks5lem1  42187  aks5lem2  42188  aks5lem3a  42190  grpods  42195  unitscyglem1  42196  unitscyglem2  42197  unitscyglem4  42199  unitscyglem5  42200  aks5  42205  metakunt1  42206  metakunt2  42207  metakunt3  42208  metakunt4  42209  metakunt5  42210  metakunt7  42212  metakunt10  42215  metakunt15  42220  metakunt16  42221  metakunt18  42223  metakunt19  42224  metakunt20  42225  metakunt21  42226  metakunt22  42227  metakunt24  42229  metakunt25  42230  metakunt26  42231  metakunt27  42232  metakunt28  42233  metakunt29  42234  metakunt30  42235  metakunt32  42237  metakunt33  42238  sumcubes  42347  oexpreposd  42357  explt1d  42358  expeq1d  42359  expeqidd  42360  exp11d  42361  gcdle1d  42365  gcdle2d  42366  dvdsexpnn0  42369  fimgmcyc  42544  fltdvdsabdvdsc  42648  fltaccoprm  42650  fltbccoprm  42651  fltabcoprm  42652  fltne  42654  flt4lem2  42657  flt4lem3  42658  flt4lem4  42659  flt4lem5  42660  flt4lem5elem  42661  flt4lem5a  42662  flt4lem5b  42663  flt4lem5c  42664  flt4lem5d  42665  flt4lem5e  42666  flt4lem5f  42667  flt4lem6  42668  flt4lem7  42669  nna4b4nsq  42670  fltltc  42671  fltnlta  42673  irrapxlem3  42835  irrapxlem5  42837  pellexlem5  42844  pellexlem6  42845  pellex  42846  pell1234qrmulcl  42866  jm2.23  43008  jm2.20nn  43009  jm2.26lem3  43013  jm2.27a  43017  jm2.27b  43018  jm2.27c  43019  jm3.1lem1  43029  jm3.1lem3  43031  inductionexd  44168  nznngen  44335  hashnzfz2  44340  fmuldfeq  45598  divcnvg  45642  stoweidlem1  46016  stoweidlem3  46018  stoweidlem11  46026  stoweidlem20  46035  stoweidlem26  46041  stoweidlem34  46049  stoweidlem51  46066  stirlinglem4  46092  stirlinglem5  46093  stirlinglem8  46096  dirkerper  46111  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  dirkercncflem2  46119  fourierdlem11  46133  fourierdlem14  46136  fourierdlem20  46142  fourierdlem25  46147  fourierdlem37  46159  fourierdlem41  46163  fourierdlem48  46169  fourierdlem49  46170  fourierdlem54  46175  fourierdlem64  46185  fourierdlem73  46194  fourierdlem79  46200  fourierdlem92  46213  fourierdlem93  46214  fourierdlem111  46232  sqwvfourb  46244  etransclem3  46252  etransclem7  46256  etransclem10  46259  etransclem15  46264  etransclem24  46273  etransclem25  46274  etransclem26  46275  etransclem27  46276  etransclem28  46277  etransclem35  46284  etransclem37  46286  etransclem38  46287  etransclem41  46290  etransclem44  46293  etransclem45  46294  etransclem48  46297  ovnsubaddlem1  46585  vonioolem1  46695  iccpartgtprec  47407  iccpartipre  47408  fmtnoodd  47520  goldbachthlem2  47533  goldbachth  47534  odz2prm2pw  47550  fmtnoprmfac1lem  47551  fmtnoprmfac2lem1  47553  fmtnoprmfac2  47554  fmtnofac2lem  47555  2pwp1prm  47576  lighneallem1  47592  lighneallem4  47597  proththdlem  47600  proththd  47601  divgcdoddALTV  47669  perfectALTVlem1  47708  perfectALTVlem2  47709  perfectALTV  47710  gbowge7  47750  gpgedgvtx1  48020  gpg3kgrtriexlem2  48040  gpg3kgrtriexlem5  48043  pw2m1lepw2m1  48437  nnolog2flm1  48511  dignn0fr  48522  dignn0flhalflem1  48536