Theorem nnzd 12584

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℕcn 12211  ℤcz 12557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7724  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-i2m1 11177  ax-1ne0 11178  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7411  df-om 7855  df-2nd 7975  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-neg 11446  df-nn 12212  df-n0 12472  df-z 12558

This theorem is referenced by:  expaddzlem  14070  expmulz  14073  expmulnbnd  14197  facndiv  14247  bcval5  14277  bcpasc  14280  hashf1  14417  isercolllem1  15610  isercolllem2  15611  o1fsum  15758  bcxmas  15780  climcndslem2  15795  climcnds  15796  mertenslem1  15829  fprodser  15892  bpolydiflem  15997  eftlub  16051  eirrlem  16146  rpnnen2lem7  16162  rpnnen2lem9  16164  rpnnen2lem11  16166  sqrt2irrlem  16190  dvdsfac  16268  dvdsmod  16271  oddpwp1fsum  16334  bitsfzolem  16374  bitsmod  16376  bitsfi  16377  bitscmp  16378  bitsinv1  16382  sadadd3  16401  sadaddlem  16406  bitsuz  16414  bitsshft  16415  gcdnncl  16447  gcd1  16468  dvdsgcdidd  16478  bezoutlem3  16482  bezoutlem4  16483  mulgcd  16489  rplpwr  16498  rprpwr  16499  sqgcd  16501  dvdssq  16503  lcmneg  16539  lcmgcdlem  16542  rpdvds  16596  coprmprod  16597  coprmproddvdslem  16598  congr  16600  cncongr1  16603  cncongr2  16604  prmz  16611  prmind2  16621  divgcdodd  16646  isprm6  16650  prmexpb  16656  prmfac1  16657  rpexp  16658  prmdvdsncoprmbd  16662  numdensq  16689  hashdvds  16707  phiprmpw  16708  crth  16710  phimullem  16711  eulerthlem1  16713  eulerthlem2  16714  prmdivdiv  16719  hashgcdlem  16720  odzdvds  16727  pythagtriplem4  16751  pythagtriplem6  16753  pythagtriplem7  16754  pythagtriplem11  16757  pythagtriplem13  16759  pythagtriplem19  16765  pclem  16770  pcprendvds2  16773  pcpre1  16774  pcpremul  16775  pceulem  16777  pcqmul  16785  pcdvdsb  16801  pcidlem  16804  pcdvdstr  16808  pcgcd1  16809  pc2dvds  16811  pcprmpw2  16814  pcaddlem  16820  pcadd  16821  pcmpt2  16825  pcmptdvds  16826  pcfac  16831  pcbc  16832  qexpz  16833  oddprmdvds  16835  prmpwdvds  16836  pockthlem  16837  pockthg  16838  prmreclem2  16849  prmreclem3  16850  prmreclem4  16851  prmreclem5  16852  prmreclem6  16853  4sqlem5  16874  4sqlem8  16877  4sqlem9  16878  4sqlem10  16879  4sqlem12  16888  4sqlem14  16890  4sqlem16  16892  4sqlem17  16893  vdwlem1  16913  vdwlem2  16914  vdwlem3  16915  vdwlem6  16918  vdwlem9  16921  vdwlem10  16922  vdwnnlem3  16929  prmdvdsprmop  16975  prmolelcmf  16980  prmgaplem1  16981  prmgaplem7  16989  prmgaplem8  16990  gsumwsubmcl  18717  gsumsgrpccat  18720  gsumwmhm  18725  mulgneg  18971  mulgnndir  18982  psgnunilem4  19364  odlem2  19406  mndodconglem  19408  odmod  19413  gexlem2  19449  gexcl3  19454  gexcl2  19456  sylow1lem1  19465  sylow1lem3  19467  sylow1lem5  19469  pgpfi  19472  fislw  19492  sylow3lem4  19497  gexexlem  19719  ablfacrplem  19934  ablfacrp  19935  ablfacrp2  19936  ablfac1lem  19937  ablfac1b  19939  ablfac1eu  19942  pgpfac1lem3a  19945  ablfaclem3  19956  fincygsubgd  19980  fincygsubgodd  19981  znrrg  21120  cayhamlem1  22367  caublcls  24825  ovolicc2lem4  25036  iundisj2  25065  volsup  25072  uniioombllem3  25101  mbfi1fseqlem3  25234  mbfi1fseqlem4  25235  elqaalem2  25832  aalioulem1  25844  aalioulem4  25847  aalioulem5  25848  aalioulem6  25849  aaliou  25850  aaliou3lem1  25854  aaliou3lem2  25855  aaliou3lem3  25856  aaliou3lem8  25857  aaliou3lem5  25859  aaliou3lem6  25860  aaliou3lem7  25861  taylthlem2  25885  cxpeq  26262  amgmlem  26491  lgamgulmlem4  26533  lgamcvg2  26556  wilthlem2  26570  wilth  26572  wilthimp  26573  ftalem5  26578  basellem2  26583  basellem3  26584  basellem4  26585  basellem5  26586  muval1  26634  dvdssqf  26639  sgmnncl  26648  efchtdvds  26660  mumullem2  26681  mumul  26682  sqff1o  26683  fsumdvdsdiaglem  26684  dvdsppwf1o  26687  dvdsflf1o  26688  muinv  26694  dvdsmulf1o  26695  chtublem  26711  fsumvma2  26714  vmasum  26716  chpchtsum  26719  logfacubnd  26721  mersenne  26727  perfect1  26728  perfectlem1  26729  perfectlem2  26730  perfect  26731  dchrelbas4  26743  dchrfi  26755  bcmono  26777  bcp1ctr  26779  bclbnd  26780  bposlem1  26784  bposlem3  26786  bposlem5  26788  bposlem6  26789  bposlem9  26792  lgsmod  26823  lgsdir  26832  lgsdilem2  26833  lgsne0  26835  lgsqrlem2  26847  lgsqr  26851  lgsqrmodndvds  26853  gausslemma2dlem0c  26858  gausslemma2dlem0h  26863  gausslemma2dlem0i  26864  gausslemma2dlem2  26867  gausslemma2dlem6  26872  gausslemma2dlem7  26873  gausslemma2d  26874  lgseisenlem1  26875  lgseisenlem2  26876  lgseisenlem3  26877  lgseisenlem4  26878  lgsquadlem1  26880  lgsquadlem2  26881  lgsquadlem3  26882  lgsquad2lem1  26884  lgsquad2lem2  26885  lgsquad2  26886  m1lgs  26888  2lgslem2  26895  2sqlem3  26920  2sqlem4  26921  2sqlem8  26926  chebbnd1lem1  26969  rplogsumlem2  26985  rpvmasumlem  26987  dchrisumlem1  26989  dchrisumlem2  26990  dchrisumlem3  26991  dchrisum0fmul  27006  dchrisum0ff  27007  dchrisum0flblem1  27008  dchrisum0flblem2  27009  dchrisum0flb  27010  dchrisum0  27020  pntrsumbnd2  27067  pntrlog2bndlem1  27077  pntrlog2bndlem6  27083  pntpbnd2  27087  pntlemg  27098  pntlemj  27103  pntlemf  27105  ostth2lem2  27134  ostth2lem3  27135  ostth3  27138  numclwlk2lem2f1o  29629  minvecolem4  30128  iundisj2f  31816  ssnnssfz  31993  iundisj2fi  32003  f1ocnt  32008  prmdvdsbc  32017  numdenneg  32018  ltesubnnd  32023  psgnfzto1stlem  32254  isarchi3  32328  archiabllem1b  32333  smatrcl  32771  1smat1  32779  submateqlem1  32782  lmatfvlem  32790  qqhval2  32957  qqhf  32961  qqhghm  32963  qqhrhm  32964  qqhnm  32965  qqhre  32995  esumcvg  33079  meascnbl  33212  omssubadd  33294  oddpwdc  33348  ballotlemfp1  33485  ballotlemfc0  33486  ballotlemfcc  33487  ballotlemimin  33499  ballotlemic  33500  ballotlem1c  33501  hgt750lemc  33654  hgt750lemd  33655  hgt750lemb  33663  hgt750leme  33665  subfaclim  34174  cvmliftlem7  34277  sinccvglem  34652  bcprod  34703  bccolsum  34704  faclimlem2  34709  faclim2  34713  poimirlem1  36484  poimirlem2  36485  poimirlem3  36486  poimirlem4  36487  poimirlem6  36489  poimirlem8  36491  poimirlem9  36492  poimirlem10  36493  poimirlem11  36494  poimirlem13  36496  poimirlem14  36497  poimirlem15  36498  poimirlem16  36499  poimirlem17  36500  poimirlem18  36501  poimirlem19  36502  poimirlem20  36503  poimirlem21  36504  poimirlem22  36505  poimirlem23  36506  poimirlem24  36507  poimirlem26  36509  poimirlem27  36510  poimirlem28  36511  poimirlem31  36514  mblfinlem2  36521  seqpo  36610  incsequz  36611  incsequz2  36612  bccl2d  40852  nnproddivdvdsd  40861  lcmineqlem1  40889  lcmineqlem3  40891  lcmineqlem4  40892  lcmineqlem6  40894  lcmineqlem8  40896  lcmineqlem9  40897  lcmineqlem10  40898  lcmineqlem11  40899  lcmineqlem13  40901  lcmineqlem14  40902  lcmineqlem18  40906  lcmineqlem19  40907  lcmineqlem20  40908  lcmineqlem21  40909  lcmineqlem22  40910  lcmineqlem23  40911  lcmineqlem  40912  3lexlogpow5ineq2  40915  3lexlogpow2ineq1  40918  aks4d1p3  40938  aks4d1p5  40940  aks4d1p6  40941  aks4d1p8d1  40944  aks4d1p8d2  40945  aks4d1p8d3  40946  aks4d1p8  40947  aks4d1p9  40948  aks6d1c2p2  40952  sticksstones6  40962  sticksstones10  40966  sticksstones12a  40968  sticksstones12  40969  metakunt1  40980  metakunt2  40981  metakunt3  40982  metakunt4  40983  metakunt5  40984  metakunt7  40986  metakunt10  40989  metakunt15  40994  metakunt16  40995  metakunt18  40997  metakunt19  40998  metakunt20  40999  metakunt21  41000  metakunt22  41001  metakunt24  41003  metakunt25  41004  metakunt26  41005  metakunt27  41006  metakunt28  41007  metakunt29  41008  metakunt30  41009  metakunt32  41011  metakunt33  41012  sumcubes  41211  oexpreposd  41212  exp11d  41216  gcdle1d  41221  gcdle2d  41222  expgcd  41225  nn0expgcd  41226  numdenexp  41228  dvdsexpnn0  41232  zrtelqelz  41236  fltdvdsabdvdsc  41381  fltaccoprm  41383  fltbccoprm  41384  fltabcoprm  41385  fltne  41387  flt4lem2  41390  flt4lem3  41391  flt4lem4  41392  flt4lem5  41393  flt4lem5elem  41394  flt4lem5a  41395  flt4lem5b  41396  flt4lem5c  41397  flt4lem5d  41398  flt4lem5e  41399  flt4lem5f  41400  flt4lem6  41401  flt4lem7  41402  nna4b4nsq  41403  fltltc  41404  fltnlta  41406  irrapxlem3  41552  irrapxlem5  41554  pellexlem5  41561  pellexlem6  41562  pellex  41563  pell1234qrmulcl  41583  jm2.23  41725  jm2.20nn  41726  jm2.26lem3  41730  jm2.27a  41734  jm2.27b  41735  jm2.27c  41736  jm3.1lem1  41746  jm3.1lem3  41748  inductionexd  42896  nznngen  43065  hashnzfz2  43070  fmuldfeq  44289  divcnvg  44333  stoweidlem1  44707  stoweidlem3  44709  stoweidlem11  44717  stoweidlem20  44726  stoweidlem26  44732  stoweidlem34  44740  stoweidlem51  44757  stirlinglem4  44783  stirlinglem5  44784  stirlinglem8  44787  dirkerper  44802  dirkertrigeqlem2  44805  dirkertrigeqlem3  44806  dirkercncflem2  44810  fourierdlem11  44824  fourierdlem14  44827  fourierdlem20  44833  fourierdlem25  44838  fourierdlem37  44850  fourierdlem41  44854  fourierdlem48  44860  fourierdlem49  44861  fourierdlem54  44866  fourierdlem64  44876  fourierdlem73  44885  fourierdlem79  44891  fourierdlem92  44904  fourierdlem93  44905  fourierdlem111  44923  sqwvfourb  44935  etransclem3  44943  etransclem7  44947  etransclem10  44950  etransclem15  44955  etransclem24  44964  etransclem25  44965  etransclem26  44966  etransclem27  44967  etransclem28  44968  etransclem35  44975  etransclem37  44977  etransclem38  44978  etransclem41  44981  etransclem44  44984  etransclem45  44985  etransclem48  44988  ovnsubaddlem1  45276  vonioolem1  45386  iccpartgtprec  46078  iccpartipre  46079  fmtnoodd  46191  goldbachthlem2  46204  goldbachth  46205  odz2prm2pw  46221  fmtnoprmfac1lem  46222  fmtnoprmfac2lem1  46224  fmtnoprmfac2  46225  fmtnofac2lem  46226  2pwp1prm  46247  lighneallem1  46263  lighneallem4  46268  proththdlem  46271  proththd  46272  divgcdoddALTV  46340  perfectALTVlem1  46379  perfectALTVlem2  46380  perfectALTV  46381  gbowge7  46421  pw2m1lepw2m1  47191  nnolog2flm1  47266  dignn0fr  47277  dignn0flhalflem1  47291