Theorem nnzd 12541

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℕcn 12165  ℤcz 12515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-i2m1 11097  ax-1ne0 11098  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-neg 11371  df-nn 12166  df-n0 12429  df-z 12516

This theorem is referenced by:  expaddzlem  14058  expmulz  14061  expmulnbnd  14188  facndiv  14241  bcval5  14271  bcpasc  14274  hashf1  14410  isercolllem1  15618  isercolllem2  15619  o1fsum  15767  bcxmas  15791  climcndslem2  15806  climcnds  15807  mertenslem1  15840  fprodser  15905  bpolydiflem  16010  eftlub  16067  eirrlem  16162  rpnnen2lem7  16178  rpnnen2lem9  16180  rpnnen2lem11  16182  sqrt2irrlem  16206  dvdsfac  16286  dvdsmod  16289  oddpwp1fsum  16352  bitsfzolem  16394  bitsmod  16396  bitsfi  16397  bitscmp  16398  bitsinv1  16402  sadadd3  16421  sadaddlem  16426  bitsuz  16434  bitsshft  16435  gcdnncl  16467  gcd1  16488  dvdsgcdidd  16497  bezoutlem3  16501  bezoutlem4  16502  mulgcd  16508  rplpwr  16518  rprpwr  16519  sqgcd  16522  expgcd  16523  nn0expgcd  16524  dvdssq  16527  lcmneg  16563  lcmgcdlem  16566  rpdvds  16620  coprmprod  16621  coprmproddvdslem  16622  congr  16624  cncongr1  16627  cncongr2  16628  prmz  16635  prmind2  16645  divgcdodd  16671  isprm6  16675  prmexpb  16680  prmfac1  16681  rpexp  16683  prmdvdsbc  16687  prmdvdsncoprmbd  16688  numdensq  16715  numdenexp  16721  hashdvds  16736  phiprmpw  16737  crth  16739  phimullem  16740  eulerthlem1  16742  eulerthlem2  16743  prmdivdiv  16748  hashgcdlem  16749  odzdvds  16757  pythagtriplem4  16781  pythagtriplem6  16783  pythagtriplem7  16784  pythagtriplem11  16787  pythagtriplem13  16789  pythagtriplem19  16795  pclem  16800  pcprendvds2  16803  pcpre1  16804  pcpremul  16805  pceulem  16807  pcqmul  16815  pcdvdsb  16831  pcidlem  16834  pcdvdstr  16838  pcgcd1  16839  pc2dvds  16841  pcprmpw2  16844  pcaddlem  16850  pcadd  16851  pcmpt2  16855  pcmptdvds  16856  pcfac  16861  pcbc  16862  qexpz  16863  oddprmdvds  16865  prmpwdvds  16866  pockthlem  16867  pockthg  16868  prmreclem2  16879  prmreclem3  16880  prmreclem4  16881  prmreclem5  16882  prmreclem6  16883  4sqlem5  16904  4sqlem8  16907  4sqlem9  16908  4sqlem10  16909  4sqlem12  16918  4sqlem14  16920  4sqlem16  16922  4sqlem17  16923  vdwlem1  16943  vdwlem2  16944  vdwlem3  16945  vdwlem6  16948  vdwlem9  16951  vdwlem10  16952  vdwnnlem3  16959  prmdvdsprmop  17005  prmolelcmf  17010  prmgaplem1  17011  prmgaplem7  17019  prmgaplem8  17020  gsumwsubmcl  18796  gsumsgrpccat  18799  gsumwmhm  18804  mulgneg  19059  mulgnndir  19070  psgnunilem4  19463  odlem2  19505  mndodconglem  19507  odmod  19512  gexlem2  19548  gexcl3  19553  gexcl2  19555  sylow1lem1  19564  sylow1lem3  19566  sylow1lem5  19568  pgpfi  19571  fislw  19591  sylow3lem4  19596  gexexlem  19818  ablfacrplem  20033  ablfacrp  20034  ablfacrp2  20035  ablfac1lem  20036  ablfac1b  20038  ablfac1eu  20041  pgpfac1lem3a  20044  ablfaclem3  20055  fincygsubgd  20079  fincygsubgodd  20080  znrrg  21540  psdpw  22158  cayhamlem1  22849  caublcls  25294  ovolicc2lem4  25505  iundisj2  25534  volsup  25541  uniioombllem3  25570  mbfi1fseqlem3  25702  mbfi1fseqlem4  25703  elqaalem2  26304  aalioulem1  26316  aalioulem4  26319  aalioulem5  26320  aalioulem6  26321  aaliou  26322  aaliou3lem1  26326  aaliou3lem2  26327  aaliou3lem3  26328  aaliou3lem8  26329  aaliou3lem5  26331  aaliou3lem6  26332  aaliou3lem7  26333  taylthlem2  26357  cxpeq  26739  zrtelqelz  26740  amgmlem  26971  lgamgulmlem4  27013  lgamcvg2  27036  wilthlem2  27050  wilth  27052  wilthimp  27053  ftalem5  27058  basellem2  27063  basellem3  27064  basellem4  27065  basellem5  27066  muval1  27114  dvdssqf  27119  sgmnncl  27128  efchtdvds  27140  mumullem2  27161  mumul  27162  sqff1o  27163  fsumdvdsdiaglem  27164  dvdsppwf1o  27167  dvdsflf1o  27168  muinv  27174  mpodvdsmulf1o  27175  dvdsmulf1o  27177  chtublem  27192  fsumvma2  27195  vmasum  27197  chpchtsum  27200  logfacubnd  27202  mersenne  27208  perfect1  27209  perfectlem1  27210  perfectlem2  27211  perfect  27212  dchrelbas4  27224  dchrfi  27236  bcmono  27258  bcp1ctr  27260  bclbnd  27261  bposlem1  27265  bposlem3  27267  bposlem5  27269  bposlem6  27270  bposlem9  27273  lgsmod  27304  lgsdir  27313  lgsdilem2  27314  lgsne0  27316  lgsqrlem2  27328  lgsqr  27332  lgsqrmodndvds  27334  gausslemma2dlem0c  27339  gausslemma2dlem0h  27344  gausslemma2dlem0i  27345  gausslemma2dlem2  27348  gausslemma2dlem6  27353  gausslemma2dlem7  27354  gausslemma2d  27355  lgseisenlem1  27356  lgseisenlem2  27357  lgseisenlem3  27358  lgseisenlem4  27359  lgsquadlem1  27361  lgsquadlem2  27362  lgsquadlem3  27363  lgsquad2lem1  27365  lgsquad2lem2  27366  lgsquad2  27367  m1lgs  27369  2lgslem2  27376  2sqlem3  27401  2sqlem4  27402  2sqlem8  27407  chebbnd1lem1  27450  rplogsumlem2  27466  rpvmasumlem  27468  dchrisumlem1  27470  dchrisumlem2  27471  dchrisumlem3  27472  dchrisum0fmul  27487  dchrisum0ff  27488  dchrisum0flblem1  27489  dchrisum0flblem2  27490  dchrisum0flb  27491  dchrisum0  27501  pntrsumbnd2  27548  pntrlog2bndlem1  27558  pntrlog2bndlem6  27564  pntpbnd2  27568  pntlemg  27579  pntlemj  27584  pntlemf  27586  ostth2lem2  27615  ostth2lem3  27616  ostth3  27619  numclwlk2lem2f1o  30467  nrt2irr  30561  minvecolem4  30969  iundisj2f  32679  ssnnssfz  32879  iundisj2fi  32889  f1ocnt  32892  elq2  32904  numdenneg  32907  expgt0b  32909  ltesubnnd  32915  oexpled  32939  psgnfzto1stlem  33181  isarchi3  33268  archiabllem1b  33273  zringfrac  33637  fldextrspundgdvds  33865  cos9thpiminplylem2  33967  smatrcl  33980  1smat1  33988  submateqlem1  33991  lmatfvlem  33999  qqhval2  34166  qqhf  34170  qqhghm  34172  qqhrhm  34173  qqhnm  34174  qqhre  34204  esumcvg  34270  meascnbl  34403  omssubadd  34484  oddpwdc  34538  ballotlemfp1  34676  ballotlemfc0  34677  ballotlemfcc  34678  ballotlemimin  34690  ballotlemic  34691  ballotlem1c  34692  hgt750lemc  34831  hgt750lemd  34832  hgt750lemb  34840  hgt750leme  34842  subfaclim  35416  cvmliftlem7  35519  sinccvglem  35900  bcprod  35966  bccolsum  35967  faclimlem2  35972  faclim2  35976  poimirlem1  37988  poimirlem2  37989  poimirlem3  37990  poimirlem4  37991  poimirlem6  37993  poimirlem8  37995  poimirlem9  37996  poimirlem10  37997  poimirlem11  37998  poimirlem13  38000  poimirlem14  38001  poimirlem15  38002  poimirlem16  38003  poimirlem17  38004  poimirlem18  38005  poimirlem19  38006  poimirlem20  38007  poimirlem21  38008  poimirlem22  38009  poimirlem23  38010  poimirlem24  38011  poimirlem26  38013  poimirlem27  38014  poimirlem28  38015  poimirlem31  38018  mblfinlem2  38025  seqpo  38114  incsequz  38115  incsequz2  38116  zndvdchrrhm  42458  bccl2d  42476  nnproddivdvdsd  42485  lcmineqlem1  42514  lcmineqlem3  42516  lcmineqlem4  42517  lcmineqlem6  42519  lcmineqlem8  42521  lcmineqlem9  42522  lcmineqlem10  42523  lcmineqlem11  42524  lcmineqlem13  42526  lcmineqlem14  42527  lcmineqlem18  42531  lcmineqlem19  42532  lcmineqlem20  42533  lcmineqlem21  42534  lcmineqlem22  42535  lcmineqlem23  42536  lcmineqlem  42537  3lexlogpow5ineq2  42540  3lexlogpow2ineq1  42543  aks4d1p3  42563  aks4d1p5  42565  aks4d1p6  42566  aks4d1p8d1  42569  aks4d1p8d2  42570  aks4d1p8d3  42571  aks4d1p8  42572  aks4d1p9  42573  posbezout  42585  primrootscoprbij  42587  remexz  42589  primrootspoweq0  42591  aks6d1c1  42601  aks6d1c2p2  42604  hashscontpow1  42606  hashscontpow  42607  aks6d1c3  42608  aks6d1c4  42609  aks6d1c2lem4  42612  aks6d1c2  42615  aks6d1c5lem1  42621  sticksstones6  42636  sticksstones10  42640  sticksstones12a  42642  sticksstones12  42643  aks6d1c6lem3  42657  aks6d1c6lem4  42658  aks6d1c6isolem3  42661  aks6d1c6lem5  42662  aks6d1c7lem2  42666  aks6d1c7  42669  aks5lem1  42671  aks5lem2  42672  aks5lem3a  42674  grpods  42679  unitscyglem1  42680  unitscyglem2  42681  unitscyglem4  42683  unitscyglem5  42684  aks5  42689  sumcubes  42790  oexpreposd  42799  explt1d  42800  expeq1d  42801  expeqidd  42802  exp11d  42803  gcdle1d  42807  gcdle2d  42808  dvdsexpnn0  42811  fimgmcyc  43020  fltdvdsabdvdsc  43088  fltaccoprm  43090  fltbccoprm  43091  fltabcoprm  43092  fltne  43094  flt4lem2  43097  flt4lem3  43098  flt4lem4  43099  flt4lem5  43100  flt4lem5elem  43101  flt4lem5a  43102  flt4lem5b  43103  flt4lem5c  43104  flt4lem5d  43105  flt4lem5e  43106  flt4lem5f  43107  flt4lem6  43108  flt4lem7  43109  nna4b4nsq  43110  fltltc  43111  fltnlta  43113  irrapxlem3  43269  irrapxlem5  43271  pellexlem5  43278  pellexlem6  43279  pellex  43280  pell1234qrmulcl  43300  jm2.23  43441  jm2.20nn  43442  jm2.26lem3  43446  jm2.27a  43450  jm2.27b  43451  jm2.27c  43452  jm3.1lem1  43462  jm3.1lem3  43464  inductionexd  44599  nznngen  44760  hashnzfz2  44765  fmuldfeq  46028  divcnvg  46072  stoweidlem1  46444  stoweidlem3  46446  stoweidlem11  46454  stoweidlem20  46463  stoweidlem26  46469  stoweidlem34  46477  stoweidlem51  46494  stirlinglem4  46520  stirlinglem5  46521  stirlinglem8  46524  dirkerper  46539  dirkertrigeqlem2  46542  dirkertrigeqlem3  46543  dirkercncflem2  46547  fourierdlem11  46561  fourierdlem14  46564  fourierdlem20  46570  fourierdlem25  46575  fourierdlem37  46587  fourierdlem41  46591  fourierdlem48  46597  fourierdlem49  46598  fourierdlem54  46603  fourierdlem64  46613  fourierdlem73  46622  fourierdlem79  46628  fourierdlem92  46641  fourierdlem93  46642  fourierdlem111  46660  sqwvfourb  46672  etransclem3  46680  etransclem7  46684  etransclem10  46687  etransclem15  46692  etransclem24  46701  etransclem25  46702  etransclem26  46703  etransclem27  46704  etransclem28  46705  etransclem35  46712  etransclem37  46714  etransclem38  46715  etransclem41  46718  etransclem44  46721  etransclem45  46722  etransclem48  46725  ovnsubaddlem1  47013  vonioolem1  47123  facnn0dvdsfac  47848  muldvdsfacgt  47849  muldvdsfacm1  47850  iccpartgtprec  47895  iccpartipre  47896  fmtnoodd  48011  goldbachthlem2  48024  goldbachth  48025  odz2prm2pw  48041  fmtnoprmfac1lem  48042  fmtnoprmfac2lem1  48044  fmtnoprmfac2  48045  fmtnofac2lem  48046  2pwp1prm  48067  lighneallem1  48083  lighneallem4  48088  proththdlem  48091  proththd  48092  nprmdvdsfacm1lem4  48101  ppivalnnprm  48103  ppivalnnnprmge6  48104  divgcdoddALTV  48173  perfectALTVlem1  48212  perfectALTVlem2  48213  perfectALTV  48214  gbowge7  48254  gpgedgvtx1  48553  gpg3kgrtriexlem2  48575  gpg3kgrtriexlem5  48578  pw2m1lepw2m1  49011  nnolog2flm1  49081  dignn0fr  49092  dignn0flhalflem1  49106