Theorem nnzd 12666

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℕcn 12293  ℤcz 12639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-neg 11523  df-nn 12294  df-n0 12554  df-z 12640

This theorem is referenced by:  expaddzlem  14156  expmulz  14159  expmulnbnd  14284  facndiv  14337  bcval5  14367  bcpasc  14370  hashf1  14506  isercolllem1  15713  isercolllem2  15714  o1fsum  15861  bcxmas  15883  climcndslem2  15898  climcnds  15899  mertenslem1  15932  fprodser  15997  bpolydiflem  16102  eftlub  16157  eirrlem  16252  rpnnen2lem7  16268  rpnnen2lem9  16270  rpnnen2lem11  16272  sqrt2irrlem  16296  dvdsfac  16374  dvdsmod  16377  oddpwp1fsum  16440  bitsfzolem  16480  bitsmod  16482  bitsfi  16483  bitscmp  16484  bitsinv1  16488  sadadd3  16507  sadaddlem  16512  bitsuz  16520  bitsshft  16521  gcdnncl  16553  gcd1  16574  dvdsgcdidd  16584  bezoutlem3  16588  bezoutlem4  16589  mulgcd  16595  rplpwr  16605  rprpwr  16606  sqgcd  16609  expgcd  16610  nn0expgcd  16611  dvdssq  16614  lcmneg  16650  lcmgcdlem  16653  rpdvds  16707  coprmprod  16708  coprmproddvdslem  16709  congr  16711  cncongr1  16714  cncongr2  16715  prmz  16722  prmind2  16732  divgcdodd  16757  isprm6  16761  prmexpb  16766  prmfac1  16767  rpexp  16769  prmdvdsbc  16773  prmdvdsncoprmbd  16774  numdensq  16801  numdenexp  16807  hashdvds  16822  phiprmpw  16823  crth  16825  phimullem  16826  eulerthlem1  16828  eulerthlem2  16829  prmdivdiv  16834  hashgcdlem  16835  odzdvds  16842  pythagtriplem4  16866  pythagtriplem6  16868  pythagtriplem7  16869  pythagtriplem11  16872  pythagtriplem13  16874  pythagtriplem19  16880  pclem  16885  pcprendvds2  16888  pcpre1  16889  pcpremul  16890  pceulem  16892  pcqmul  16900  pcdvdsb  16916  pcidlem  16919  pcdvdstr  16923  pcgcd1  16924  pc2dvds  16926  pcprmpw2  16929  pcaddlem  16935  pcadd  16936  pcmpt2  16940  pcmptdvds  16941  pcfac  16946  pcbc  16947  qexpz  16948  oddprmdvds  16950  prmpwdvds  16951  pockthlem  16952  pockthg  16953  prmreclem2  16964  prmreclem3  16965  prmreclem4  16966  prmreclem5  16967  prmreclem6  16968  4sqlem5  16989  4sqlem8  16992  4sqlem9  16993  4sqlem10  16994  4sqlem12  17003  4sqlem14  17005  4sqlem16  17007  4sqlem17  17008  vdwlem1  17028  vdwlem2  17029  vdwlem3  17030  vdwlem6  17033  vdwlem9  17036  vdwlem10  17037  vdwnnlem3  17044  prmdvdsprmop  17090  prmolelcmf  17095  prmgaplem1  17096  prmgaplem7  17104  prmgaplem8  17105  gsumwsubmcl  18872  gsumsgrpccat  18875  gsumwmhm  18880  mulgneg  19132  mulgnndir  19143  psgnunilem4  19539  odlem2  19581  mndodconglem  19583  odmod  19588  gexlem2  19624  gexcl3  19629  gexcl2  19631  sylow1lem1  19640  sylow1lem3  19642  sylow1lem5  19644  pgpfi  19647  fislw  19667  sylow3lem4  19672  gexexlem  19894  ablfacrplem  20109  ablfacrp  20110  ablfacrp2  20111  ablfac1lem  20112  ablfac1b  20114  ablfac1eu  20117  pgpfac1lem3a  20120  ablfaclem3  20131  fincygsubgd  20155  fincygsubgodd  20156  znrrg  21607  cayhamlem1  22893  caublcls  25362  ovolicc2lem4  25574  iundisj2  25603  volsup  25610  uniioombllem3  25639  mbfi1fseqlem3  25772  mbfi1fseqlem4  25773  elqaalem2  26380  aalioulem1  26392  aalioulem4  26395  aalioulem5  26396  aalioulem6  26397  aaliou  26398  aaliou3lem1  26402  aaliou3lem2  26403  aaliou3lem3  26404  aaliou3lem8  26405  aaliou3lem5  26407  aaliou3lem6  26408  aaliou3lem7  26409  taylthlem2  26434  taylthlem2OLD  26435  cxpeq  26818  zrtelqelz  26819  amgmlem  27051  lgamgulmlem4  27093  lgamcvg2  27116  wilthlem2  27130  wilth  27132  wilthimp  27133  ftalem5  27138  basellem2  27143  basellem3  27144  basellem4  27145  basellem5  27146  muval1  27194  dvdssqf  27199  sgmnncl  27208  efchtdvds  27220  mumullem2  27241  mumul  27242  sqff1o  27243  fsumdvdsdiaglem  27244  dvdsppwf1o  27247  dvdsflf1o  27248  muinv  27254  mpodvdsmulf1o  27255  dvdsmulf1o  27257  chtublem  27273  fsumvma2  27276  vmasum  27278  chpchtsum  27281  logfacubnd  27283  mersenne  27289  perfect1  27290  perfectlem1  27291  perfectlem2  27292  perfect  27293  dchrelbas4  27305  dchrfi  27317  bcmono  27339  bcp1ctr  27341  bclbnd  27342  bposlem1  27346  bposlem3  27348  bposlem5  27350  bposlem6  27351  bposlem9  27354  lgsmod  27385  lgsdir  27394  lgsdilem2  27395  lgsne0  27397  lgsqrlem2  27409  lgsqr  27413  lgsqrmodndvds  27415  gausslemma2dlem0c  27420  gausslemma2dlem0h  27425  gausslemma2dlem0i  27426  gausslemma2dlem2  27429  gausslemma2dlem6  27434  gausslemma2dlem7  27435  gausslemma2d  27436  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem3  27439  lgseisenlem4  27440  lgsquadlem1  27442  lgsquadlem2  27443  lgsquadlem3  27444  lgsquad2lem1  27446  lgsquad2lem2  27447  lgsquad2  27448  m1lgs  27450  2lgslem2  27457  2sqlem3  27482  2sqlem4  27483  2sqlem8  27488  chebbnd1lem1  27531  rplogsumlem2  27547  rpvmasumlem  27549  dchrisumlem1  27551  dchrisumlem2  27552  dchrisumlem3  27553  dchrisum0fmul  27568  dchrisum0ff  27569  dchrisum0flblem1  27570  dchrisum0flblem2  27571  dchrisum0flb  27572  dchrisum0  27582  pntrsumbnd2  27629  pntrlog2bndlem1  27639  pntrlog2bndlem6  27645  pntpbnd2  27649  pntlemg  27660  pntlemj  27665  pntlemf  27667  ostth2lem2  27696  ostth2lem3  27697  ostth3  27700  numclwlk2lem2f1o  30411  nrt2irr  30505  minvecolem4  30912  iundisj2f  32612  ssnnssfz  32792  iundisj2fi  32802  f1ocnt  32807  numdenneg  32818  expgt0b  32820  ltesubnnd  32826  psgnfzto1stlem  33093  isarchi3  33167  archiabllem1b  33172  zringfrac  33547  smatrcl  33742  1smat1  33750  submateqlem1  33753  lmatfvlem  33761  qqhval2  33928  qqhf  33932  qqhghm  33934  qqhrhm  33935  qqhnm  33936  qqhre  33966  esumcvg  34050  meascnbl  34183  omssubadd  34265  oddpwdc  34319  ballotlemfp1  34456  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemimin  34470  ballotlemic  34471  ballotlem1c  34472  hgt750lemc  34624  hgt750lemd  34625  hgt750lemb  34633  hgt750leme  34635  subfaclim  35156  cvmliftlem7  35259  sinccvglem  35640  bcprod  35700  bccolsum  35701  faclimlem2  35706  faclim2  35710  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem6  37586  poimirlem8  37588  poimirlem9  37589  poimirlem10  37590  poimirlem11  37591  poimirlem13  37593  poimirlem14  37594  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem23  37603  poimirlem24  37604  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  poimirlem31  37611  mblfinlem2  37618  seqpo  37707  incsequz  37708  incsequz2  37709  zndvdchrrhm  41927  bccl2d  41948  nnproddivdvdsd  41957  lcmineqlem1  41986  lcmineqlem3  41988  lcmineqlem4  41989  lcmineqlem6  41991  lcmineqlem8  41993  lcmineqlem9  41994  lcmineqlem10  41995  lcmineqlem11  41996  lcmineqlem13  41998  lcmineqlem14  41999  lcmineqlem18  42003  lcmineqlem19  42004  lcmineqlem20  42005  lcmineqlem21  42006  lcmineqlem22  42007  lcmineqlem23  42008  lcmineqlem  42009  3lexlogpow5ineq2  42012  3lexlogpow2ineq1  42015  aks4d1p3  42035  aks4d1p5  42037  aks4d1p6  42038  aks4d1p8d1  42041  aks4d1p8d2  42042  aks4d1p8d3  42043  aks4d1p8  42044  aks4d1p9  42045  posbezout  42057  primrootscoprbij  42059  remexz  42061  primrootspoweq0  42063  aks6d1c1  42073  aks6d1c2p2  42076  hashscontpow1  42078  hashscontpow  42079  aks6d1c3  42080  aks6d1c4  42081  aks6d1c2lem4  42084  aks6d1c2  42087  aks6d1c5lem1  42093  sticksstones6  42108  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  aks6d1c6lem3  42129  aks6d1c6lem4  42130  aks6d1c6isolem3  42133  aks6d1c6lem5  42134  aks6d1c7lem2  42138  aks6d1c7  42141  aks5lem1  42143  aks5lem2  42144  aks5lem3a  42146  grpods  42151  unitscyglem1  42152  unitscyglem2  42153  unitscyglem4  42155  unitscyglem5  42156  aks5  42161  metakunt1  42162  metakunt2  42163  metakunt3  42164  metakunt4  42165  metakunt5  42166  metakunt7  42168  metakunt10  42171  metakunt15  42176  metakunt16  42177  metakunt18  42179  metakunt19  42180  metakunt20  42181  metakunt21  42182  metakunt22  42183  metakunt24  42185  metakunt25  42186  metakunt26  42187  metakunt27  42188  metakunt28  42189  metakunt29  42190  metakunt30  42191  metakunt32  42193  metakunt33  42194  sumcubes  42301  oexpreposd  42309  explt1d  42310  expeq1d  42311  expeqidd  42312  exp11d  42313  gcdle1d  42317  gcdle2d  42318  dvdsexpnn0  42321  fimgmcyc  42489  fltdvdsabdvdsc  42593  fltaccoprm  42595  fltbccoprm  42596  fltabcoprm  42597  fltne  42599  flt4lem2  42602  flt4lem3  42603  flt4lem4  42604  flt4lem5  42605  flt4lem5elem  42606  flt4lem5a  42607  flt4lem5b  42608  flt4lem5c  42609  flt4lem5d  42610  flt4lem5e  42611  flt4lem5f  42612  flt4lem6  42613  flt4lem7  42614  nna4b4nsq  42615  fltltc  42616  fltnlta  42618  irrapxlem3  42780  irrapxlem5  42782  pellexlem5  42789  pellexlem6  42790  pellex  42791  pell1234qrmulcl  42811  jm2.23  42953  jm2.20nn  42954  jm2.26lem3  42958  jm2.27a  42962  jm2.27b  42963  jm2.27c  42964  jm3.1lem1  42974  jm3.1lem3  42976  inductionexd  44117  nznngen  44285  hashnzfz2  44290  fmuldfeq  45504  divcnvg  45548  stoweidlem1  45922  stoweidlem3  45924  stoweidlem11  45932  stoweidlem20  45941  stoweidlem26  45947  stoweidlem34  45955  stoweidlem51  45972  stirlinglem4  45998  stirlinglem5  45999  stirlinglem8  46002  dirkerper  46017  dirkertrigeqlem2  46020  dirkertrigeqlem3  46021  dirkercncflem2  46025  fourierdlem11  46039  fourierdlem14  46042  fourierdlem20  46048  fourierdlem25  46053  fourierdlem37  46065  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem54  46081  fourierdlem64  46091  fourierdlem73  46100  fourierdlem79  46106  fourierdlem92  46119  fourierdlem93  46120  fourierdlem111  46138  sqwvfourb  46150  etransclem3  46158  etransclem7  46162  etransclem10  46165  etransclem15  46170  etransclem24  46179  etransclem25  46180  etransclem26  46181  etransclem27  46182  etransclem28  46183  etransclem35  46190  etransclem37  46192  etransclem38  46193  etransclem41  46196  etransclem44  46199  etransclem45  46200  etransclem48  46203  ovnsubaddlem1  46491  vonioolem1  46601  iccpartgtprec  47294  iccpartipre  47295  fmtnoodd  47407  goldbachthlem2  47420  goldbachth  47421  odz2prm2pw  47437  fmtnoprmfac1lem  47438  fmtnoprmfac2lem1  47440  fmtnoprmfac2  47441  fmtnofac2lem  47442  2pwp1prm  47463  lighneallem1  47479  lighneallem4  47484  proththdlem  47487  proththd  47488  divgcdoddALTV  47556  perfectALTVlem1  47595  perfectALTVlem2  47596  perfectALTV  47597  gbowge7  47637  pw2m1lepw2m1  48249  nnolog2flm1  48324  dignn0fr  48335  dignn0flhalflem1  48349