Theorem nnzd 12588

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℕcn 12204  ℤcz 12562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387  ax-un 7713  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-i2m1 11135  ax-1ne0 11136  ax-rnegex 11138  ax-rrecex 11139  ax-cnre 11140

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-ov 7394  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-neg 11411  df-nn 12205  df-n0 12476  df-z 12563

This theorem is referenced by:  expaddzlem  14112  expmulz  14115  expmulnbnd  14242  facndiv  14295  bcval5  14325  bcpasc  14328  hashf1  14464  isercolllem1  15683  isercolllem2  15684  o1fsum  15832  bcxmas  15856  climcndslem2  15871  climcnds  15872  mertenslem1  15905  fprodser  15970  bpolydiflem  16075  eftlub  16132  eirrlem  16227  rpnnen2lem7  16243  rpnnen2lem9  16245  rpnnen2lem11  16247  sqrt2irrlem  16271  dvdsfac  16351  dvdsmod  16354  oddpwp1fsum  16417  bitsfzolem  16459  bitsmod  16461  bitsfi  16462  bitscmp  16463  bitsinv1  16467  sadadd3  16486  sadaddlem  16491  bitsuz  16499  bitsshft  16500  gcdnncl  16532  gcd1  16553  dvdsgcdidd  16562  bezoutlem3  16566  bezoutlem4  16567  mulgcd  16573  rplpwr  16583  rprpwr  16584  sqgcd  16587  expgcd  16588  nn0expgcd  16589  dvdssq  16592  lcmneg  16628  lcmgcdlem  16631  rpdvds  16685  coprmprod  16686  coprmproddvdslem  16687  congr  16689  cncongr1  16692  cncongr2  16693  prmz  16700  prmind2  16710  divgcdodd  16736  isprm6  16740  prmexpb  16745  prmfac1  16746  rpexp  16748  prmdvdsbc  16752  prmdvdsncoprmbd  16753  numdensq  16780  numdenexp  16786  hashdvds  16801  phiprmpw  16802  crth  16804  phimullem  16805  eulerthlem1  16807  eulerthlem2  16808  prmdivdiv  16813  hashgcdlem  16814  odzdvds  16822  pythagtriplem4  16846  pythagtriplem6  16848  pythagtriplem7  16849  pythagtriplem11  16852  pythagtriplem13  16854  pythagtriplem19  16860  pclem  16865  pcprendvds2  16868  pcpre1  16869  pcpremul  16870  pceulem  16872  pcqmul  16880  pcdvdsb  16896  pcidlem  16899  pcdvdstr  16903  pcgcd1  16904  pc2dvds  16906  pcprmpw2  16909  pcaddlem  16915  pcadd  16916  pcmpt2  16920  pcmptdvds  16921  pcfac  16926  pcbc  16927  qexpz  16928  oddprmdvds  16930  prmpwdvds  16931  pockthlem  16932  pockthg  16933  prmreclem2  16944  prmreclem3  16945  prmreclem4  16946  prmreclem5  16947  prmreclem6  16948  4sqlem5  16969  4sqlem8  16972  4sqlem9  16973  4sqlem10  16974  4sqlem12  16983  4sqlem14  16985  4sqlem16  16987  4sqlem17  16988  vdwlem1  17008  vdwlem2  17009  vdwlem3  17010  vdwlem6  17013  vdwlem9  17016  vdwlem10  17017  vdwnnlem3  17024  prmdvdsprmop  17070  prmolelcmf  17075  prmgaplem1  17076  prmgaplem7  17084  prmgaplem8  17085  gsumwsubmcl  18862  gsumsgrpccat  18865  gsumwmhm  18870  mulgneg  19125  mulgnndir  19136  psgnunilem4  19528  odlem2  19570  mndodconglem  19572  odmod  19577  gexlem2  19613  gexcl3  19618  gexcl2  19620  sylow1lem1  19629  sylow1lem3  19631  sylow1lem5  19633  pgpfi  19636  fislw  19656  sylow3lem4  19661  gexexlem  19883  ablfacrplem  20098  ablfacrp  20099  ablfacrp2  20100  ablfac1lem  20101  ablfac1b  20103  ablfac1eu  20106  pgpfac1lem3a  20109  ablfaclem3  20120  fincygsubgd  20144  fincygsubgodd  20145  znrrg  21605  psdpw  22223  cayhamlem1  22914  caublcls  25359  ovolicc2lem4  25570  iundisj2  25599  volsup  25606  uniioombllem3  25635  mbfi1fseqlem3  25767  mbfi1fseqlem4  25768  elqaalem2  26372  aalioulem1  26384  aalioulem4  26387  aalioulem5  26388  aalioulem6  26389  aaliou  26390  aaliou3lem1  26394  aaliou3lem2  26395  aaliou3lem3  26396  aaliou3lem8  26397  aaliou3lem5  26399  aaliou3lem6  26400  aaliou3lem7  26401  taylthlem2  26425  cxpeq  26810  zrtelqelz  26811  amgmlem  27042  lgamgulmlem4  27084  lgamcvg2  27107  wilthlem2  27121  wilth  27123  wilthimp  27124  ftalem5  27129  basellem2  27134  basellem3  27135  basellem4  27136  basellem5  27137  muval1  27185  dvdssqf  27190  sgmnncl  27199  efchtdvds  27211  mumullem2  27232  mumul  27233  sqff1o  27234  fsumdvdsdiaglem  27235  dvdsppwf1o  27238  dvdsflf1o  27239  muinv  27245  mpodvdsmulf1o  27246  dvdsmulf1o  27248  chtublem  27263  fsumvma2  27266  vmasum  27268  chpchtsum  27271  logfacubnd  27273  mersenne  27279  perfect1  27280  perfectlem1  27281  perfectlem2  27282  perfect  27283  dchrelbas4  27295  dchrfi  27307  bcmono  27329  bcp1ctr  27331  bclbnd  27332  bposlem1  27336  bposlem3  27338  bposlem5  27340  bposlem6  27341  bposlem9  27344  lgsmod  27375  lgsdir  27384  lgsdilem2  27385  lgsne0  27387  lgsqrlem2  27399  lgsqr  27403  lgsqrmodndvds  27405  gausslemma2dlem0c  27410  gausslemma2dlem0h  27415  gausslemma2dlem0i  27416  gausslemma2dlem2  27419  gausslemma2dlem6  27424  gausslemma2dlem7  27425  gausslemma2d  27426  lgseisenlem1  27427  lgseisenlem2  27428  lgseisenlem3  27429  lgseisenlem4  27430  lgsquadlem1  27432  lgsquadlem2  27433  lgsquadlem3  27434  lgsquad2lem1  27436  lgsquad2lem2  27437  lgsquad2  27438  m1lgs  27440  2lgslem2  27447  2sqlem3  27472  2sqlem4  27473  2sqlem8  27478  chebbnd1lem1  27521  rplogsumlem2  27537  rpvmasumlem  27539  dchrisumlem1  27541  dchrisumlem2  27542  dchrisumlem3  27543  dchrisum0fmul  27558  dchrisum0ff  27559  dchrisum0flblem1  27560  dchrisum0flblem2  27561  dchrisum0flb  27562  dchrisum0  27572  pntrsumbnd2  27619  pntrlog2bndlem1  27629  pntrlog2bndlem6  27635  pntpbnd2  27639  pntlemg  27650  pntlemj  27655  pntlemf  27657  ostth2lem2  27686  ostth2lem3  27687  ostth3  27690  numclwlk2lem2f1o  30538  nrt2irr  30632  minvecolem4  31040  iundisj2f  32750  ssnnssfz  32950  iundisj2fi  32960  f1ocnt  32963  elq2  32975  numdenneg  32978  expgt0b  32980  ltesubnnd  32986  oexpled  32999  psgnfzto1stlem  33241  isarchi3  33328  archiabllem1b  33333  zringfrac  33711  fldextrspundgdvds  33939  cos9thpiminplylem2  34041  smatrcl  34054  1smat1  34062  submateqlem1  34065  lmatfvlem  34073  qqhval2  34240  qqhf  34244  qqhghm  34246  qqhrhm  34247  qqhnm  34248  qqhre  34278  esumcvg  34344  meascnbl  34477  omssubadd  34558  oddpwdc  34612  ballotlemfp1  34750  ballotlemfc0  34751  ballotlemfcc  34752  ballotlemimin  34764  ballotlemic  34765  ballotlem1c  34766  hgt750lemc  34902  hgt750lemd  34903  hgt750lemb  34911  hgt750leme  34913  subfaclim  35499  cvmliftlem7  35602  sinccvglem  35983  bcprod  36049  bccolsum  36050  faclimlem2  36055  faclim2  36059  poimirlem1  38081  poimirlem2  38082  poimirlem3  38083  poimirlem4  38084  poimirlem6  38086  poimirlem8  38088  poimirlem9  38089  poimirlem10  38090  poimirlem11  38091  poimirlem13  38093  poimirlem14  38094  poimirlem15  38095  poimirlem16  38096  poimirlem17  38097  poimirlem18  38098  poimirlem19  38099  poimirlem20  38100  poimirlem21  38101  poimirlem22  38102  poimirlem23  38103  poimirlem24  38104  poimirlem26  38106  poimirlem27  38107  poimirlem28  38108  poimirlem31  38111  mblfinlem2  38118  seqpo  38207  incsequz  38208  incsequz2  38209  zndvdchrrhm  42551  bccl2d  42569  nnproddivdvdsd  42578  lcmineqlem1  42607  lcmineqlem3  42609  lcmineqlem4  42610  lcmineqlem6  42612  lcmineqlem8  42614  lcmineqlem9  42615  lcmineqlem10  42616  lcmineqlem11  42617  lcmineqlem13  42619  lcmineqlem14  42620  lcmineqlem18  42624  lcmineqlem19  42625  lcmineqlem20  42626  lcmineqlem21  42627  lcmineqlem22  42628  lcmineqlem23  42629  lcmineqlem  42630  3lexlogpow5ineq2  42633  3lexlogpow2ineq1  42636  aks4d1p3  42656  aks4d1p5  42658  aks4d1p6  42659  aks4d1p8d1  42662  aks4d1p8d2  42663  aks4d1p8d3  42664  aks4d1p8  42665  aks4d1p9  42666  posbezout  42678  primrootscoprbij  42680  remexz  42682  primrootspoweq0  42684  aks6d1c1  42694  aks6d1c2p2  42697  hashscontpow1  42699  hashscontpow  42700  aks6d1c3  42701  aks6d1c4  42702  aks6d1c2lem4  42705  aks6d1c2  42708  aks6d1c5lem1  42714  sticksstones6  42729  sticksstones10  42733  sticksstones12a  42735  sticksstones12  42736  aks6d1c6lem3  42750  aks6d1c6lem4  42751  aks6d1c6isolem3  42754  aks6d1c6lem5  42755  aks6d1c7lem2  42759  aks6d1c7  42762  aks5lem1  42764  aks5lem2  42765  aks5lem3a  42767  grpods  42772  unitscyglem1  42773  unitscyglem2  42774  unitscyglem4  42776  unitscyglem5  42777  aks5  42782  sumcubes  42883  oexpreposd  42892  explt1d  42893  expeq1d  42894  expeqidd  42895  exp11d  42896  gcdle1d  42900  gcdle2d  42901  dvdsexpnn0  42904  fimgmcyc  43113  fltdvdsabdvdsc  43181  fltaccoprm  43183  fltbccoprm  43184  fltabcoprm  43185  fltne  43187  flt4lem2  43190  flt4lem3  43191  flt4lem4  43192  flt4lem5  43193  flt4lem5elem  43194  flt4lem5a  43195  flt4lem5b  43196  flt4lem5c  43197  flt4lem5d  43198  flt4lem5e  43199  flt4lem5f  43200  flt4lem6  43201  flt4lem7  43202  nna4b4nsq  43203  fltltc  43204  fltnlta  43206  irrapxlem3  43362  irrapxlem5  43364  pellexlem5  43371  pellexlem6  43372  pellex  43373  pell1234qrmulcl  43393  jm2.23  43534  jm2.20nn  43535  jm2.26lem3  43539  jm2.27a  43543  jm2.27b  43544  jm2.27c  43545  jm3.1lem1  43555  jm3.1lem3  43557  inductionexd  44692  nznngen  44853  hashnzfz2  44858  fmuldfeq  46120  divcnvg  46164  stoweidlem1  46536  stoweidlem3  46538  stoweidlem11  46546  stoweidlem20  46555  stoweidlem26  46561  stoweidlem34  46569  stoweidlem51  46586  stirlinglem4  46612  stirlinglem5  46613  stirlinglem8  46616  dirkerper  46631  dirkertrigeqlem2  46634  dirkertrigeqlem3  46635  dirkercncflem2  46639  fourierdlem11  46653  fourierdlem14  46656  fourierdlem20  46662  fourierdlem25  46667  fourierdlem37  46679  fourierdlem41  46683  fourierdlem48  46689  fourierdlem49  46690  fourierdlem54  46695  fourierdlem64  46705  fourierdlem73  46714  fourierdlem79  46720  fourierdlem92  46733  fourierdlem93  46734  fourierdlem111  46752  sqwvfourb  46764  etransclem3  46772  etransclem7  46776  etransclem10  46779  etransclem15  46784  etransclem24  46793  etransclem25  46794  etransclem26  46795  etransclem27  46796  etransclem28  46797  etransclem35  46804  etransclem37  46806  etransclem38  46807  etransclem41  46810  etransclem44  46813  etransclem45  46814  etransclem48  46817  ovnsubaddlem1  47105  vonioolem1  47215  facnn0dvdsfac  47940  muldvdsfacgt  47941  muldvdsfacm1  47942  iccpartgtprec  47987  iccpartipre  47988  fmtnoodd  48103  goldbachthlem2  48116  goldbachth  48117  odz2prm2pw  48133  fmtnoprmfac1lem  48134  fmtnoprmfac2lem1  48136  fmtnoprmfac2  48137  fmtnofac2lem  48138  2pwp1prm  48159  lighneallem1  48175  lighneallem4  48180  proththdlem  48183  proththd  48184  nprmdvdsfacm1lem4  48193  ppivalnnprm  48195  ppivalnnnprmge6  48196  divgcdoddALTV  48265  perfectALTVlem1  48304  perfectALTVlem2  48305  perfectALTV  48306  gbowge7  48346  gpgedgvtx1  48645  gpg3kgrtriexlem2  48667  gpg3kgrtriexlem5  48670  pw2m1lepw2m1  49103  nnolog2flm1  49173  dignn0fr  49184  dignn0flhalflem1  49198