Theorem nnzd 12526

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕcn 12157  ℤcz 12500

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-neg 11379  df-nn 12158  df-n0 12414  df-z 12501

This theorem is referenced by:  expaddzlem  14040  expmulz  14043  expmulnbnd  14170  facndiv  14223  bcval5  14253  bcpasc  14256  hashf1  14392  isercolllem1  15600  isercolllem2  15601  o1fsum  15748  bcxmas  15770  climcndslem2  15785  climcnds  15786  mertenslem1  15819  fprodser  15884  bpolydiflem  15989  eftlub  16046  eirrlem  16141  rpnnen2lem7  16157  rpnnen2lem9  16159  rpnnen2lem11  16161  sqrt2irrlem  16185  dvdsfac  16265  dvdsmod  16268  oddpwp1fsum  16331  bitsfzolem  16373  bitsmod  16375  bitsfi  16376  bitscmp  16377  bitsinv1  16381  sadadd3  16400  sadaddlem  16405  bitsuz  16413  bitsshft  16414  gcdnncl  16446  gcd1  16467  dvdsgcdidd  16476  bezoutlem3  16480  bezoutlem4  16481  mulgcd  16487  rplpwr  16497  rprpwr  16498  sqgcd  16501  expgcd  16502  nn0expgcd  16503  dvdssq  16506  lcmneg  16542  lcmgcdlem  16545  rpdvds  16599  coprmprod  16600  coprmproddvdslem  16601  congr  16603  cncongr1  16606  cncongr2  16607  prmz  16614  prmind2  16624  divgcdodd  16649  isprm6  16653  prmexpb  16658  prmfac1  16659  rpexp  16661  prmdvdsbc  16665  prmdvdsncoprmbd  16666  numdensq  16693  numdenexp  16699  hashdvds  16714  phiprmpw  16715  crth  16717  phimullem  16718  eulerthlem1  16720  eulerthlem2  16721  prmdivdiv  16726  hashgcdlem  16727  odzdvds  16735  pythagtriplem4  16759  pythagtriplem6  16761  pythagtriplem7  16762  pythagtriplem11  16765  pythagtriplem13  16767  pythagtriplem19  16773  pclem  16778  pcprendvds2  16781  pcpre1  16782  pcpremul  16783  pceulem  16785  pcqmul  16793  pcdvdsb  16809  pcidlem  16812  pcdvdstr  16816  pcgcd1  16817  pc2dvds  16819  pcprmpw2  16822  pcaddlem  16828  pcadd  16829  pcmpt2  16833  pcmptdvds  16834  pcfac  16839  pcbc  16840  qexpz  16841  oddprmdvds  16843  prmpwdvds  16844  pockthlem  16845  pockthg  16846  prmreclem2  16857  prmreclem3  16858  prmreclem4  16859  prmreclem5  16860  prmreclem6  16861  4sqlem5  16882  4sqlem8  16885  4sqlem9  16886  4sqlem10  16887  4sqlem12  16896  4sqlem14  16898  4sqlem16  16900  4sqlem17  16901  vdwlem1  16921  vdwlem2  16922  vdwlem3  16923  vdwlem6  16926  vdwlem9  16929  vdwlem10  16930  vdwnnlem3  16937  prmdvdsprmop  16983  prmolelcmf  16988  prmgaplem1  16989  prmgaplem7  16997  prmgaplem8  16998  gsumwsubmcl  18774  gsumsgrpccat  18777  gsumwmhm  18782  mulgneg  19034  mulgnndir  19045  psgnunilem4  19438  odlem2  19480  mndodconglem  19482  odmod  19487  gexlem2  19523  gexcl3  19528  gexcl2  19530  sylow1lem1  19539  sylow1lem3  19541  sylow1lem5  19543  pgpfi  19546  fislw  19566  sylow3lem4  19571  gexexlem  19793  ablfacrplem  20008  ablfacrp  20009  ablfacrp2  20010  ablfac1lem  20011  ablfac1b  20013  ablfac1eu  20016  pgpfac1lem3a  20019  ablfaclem3  20030  fincygsubgd  20054  fincygsubgodd  20055  znrrg  21532  psdpw  22125  cayhamlem1  22822  caublcls  25277  ovolicc2lem4  25489  iundisj2  25518  volsup  25525  uniioombllem3  25554  mbfi1fseqlem3  25686  mbfi1fseqlem4  25687  elqaalem2  26296  aalioulem1  26308  aalioulem4  26311  aalioulem5  26312  aalioulem6  26313  aaliou  26314  aaliou3lem1  26318  aaliou3lem2  26319  aaliou3lem3  26320  aaliou3lem8  26321  aaliou3lem5  26323  aaliou3lem6  26324  aaliou3lem7  26325  taylthlem2  26350  taylthlem2OLD  26351  cxpeq  26735  zrtelqelz  26736  amgmlem  26968  lgamgulmlem4  27010  lgamcvg2  27033  wilthlem2  27047  wilth  27049  wilthimp  27050  ftalem5  27055  basellem2  27060  basellem3  27061  basellem4  27062  basellem5  27063  muval1  27111  dvdssqf  27116  sgmnncl  27125  efchtdvds  27137  mumullem2  27158  mumul  27159  sqff1o  27160  fsumdvdsdiaglem  27161  dvdsppwf1o  27164  dvdsflf1o  27165  muinv  27171  mpodvdsmulf1o  27172  dvdsmulf1o  27174  chtublem  27190  fsumvma2  27193  vmasum  27195  chpchtsum  27198  logfacubnd  27200  mersenne  27206  perfect1  27207  perfectlem1  27208  perfectlem2  27209  perfect  27210  dchrelbas4  27222  dchrfi  27234  bcmono  27256  bcp1ctr  27258  bclbnd  27259  bposlem1  27263  bposlem3  27265  bposlem5  27267  bposlem6  27268  bposlem9  27271  lgsmod  27302  lgsdir  27311  lgsdilem2  27312  lgsne0  27314  lgsqrlem2  27326  lgsqr  27330  lgsqrmodndvds  27332  gausslemma2dlem0c  27337  gausslemma2dlem0h  27342  gausslemma2dlem0i  27343  gausslemma2dlem2  27346  gausslemma2dlem6  27351  gausslemma2dlem7  27352  gausslemma2d  27353  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem3  27356  lgseisenlem4  27357  lgsquadlem1  27359  lgsquadlem2  27360  lgsquadlem3  27361  lgsquad2lem1  27363  lgsquad2lem2  27364  lgsquad2  27365  m1lgs  27367  2lgslem2  27374  2sqlem3  27399  2sqlem4  27400  2sqlem8  27405  chebbnd1lem1  27448  rplogsumlem2  27464  rpvmasumlem  27466  dchrisumlem1  27468  dchrisumlem2  27469  dchrisumlem3  27470  dchrisum0fmul  27485  dchrisum0ff  27486  dchrisum0flblem1  27487  dchrisum0flblem2  27488  dchrisum0flb  27489  dchrisum0  27499  pntrsumbnd2  27546  pntrlog2bndlem1  27556  pntrlog2bndlem6  27562  pntpbnd2  27566  pntlemg  27577  pntlemj  27582  pntlemf  27584  ostth2lem2  27613  ostth2lem3  27614  ostth3  27617  numclwlk2lem2f1o  30466  nrt2irr  30560  minvecolem4  30968  iundisj2f  32677  ssnnssfz  32878  iundisj2fi  32888  f1ocnt  32891  elq2  32903  numdenneg  32906  expgt0b  32908  ltesubnnd  32914  oexpled  32939  psgnfzto1stlem  33194  isarchi3  33281  archiabllem1b  33286  zringfrac  33647  fldextrspundgdvds  33859  cos9thpiminplylem2  33961  smatrcl  33974  1smat1  33982  submateqlem1  33985  lmatfvlem  33993  qqhval2  34160  qqhf  34164  qqhghm  34166  qqhrhm  34167  qqhnm  34168  qqhre  34198  esumcvg  34264  meascnbl  34397  omssubadd  34478  oddpwdc  34532  ballotlemfp1  34670  ballotlemfc0  34671  ballotlemfcc  34672  ballotlemimin  34684  ballotlemic  34685  ballotlem1c  34686  hgt750lemc  34825  hgt750lemd  34826  hgt750lemb  34834  hgt750leme  34836  subfaclim  35404  cvmliftlem7  35507  sinccvglem  35888  bcprod  35954  bccolsum  35955  faclimlem2  35960  faclim2  35964  poimirlem1  37872  poimirlem2  37873  poimirlem3  37874  poimirlem4  37875  poimirlem6  37877  poimirlem8  37879  poimirlem9  37880  poimirlem10  37881  poimirlem11  37882  poimirlem13  37884  poimirlem14  37885  poimirlem15  37886  poimirlem16  37887  poimirlem17  37888  poimirlem18  37889  poimirlem19  37890  poimirlem20  37891  poimirlem21  37892  poimirlem22  37893  poimirlem23  37894  poimirlem24  37895  poimirlem26  37897  poimirlem27  37898  poimirlem28  37899  poimirlem31  37902  mblfinlem2  37909  seqpo  37998  incsequz  37999  incsequz2  38000  zndvdchrrhm  42342  bccl2d  42361  nnproddivdvdsd  42370  lcmineqlem1  42399  lcmineqlem3  42401  lcmineqlem4  42402  lcmineqlem6  42404  lcmineqlem8  42406  lcmineqlem9  42407  lcmineqlem10  42408  lcmineqlem11  42409  lcmineqlem13  42411  lcmineqlem14  42412  lcmineqlem18  42416  lcmineqlem19  42417  lcmineqlem20  42418  lcmineqlem21  42419  lcmineqlem22  42420  lcmineqlem23  42421  lcmineqlem  42422  3lexlogpow5ineq2  42425  3lexlogpow2ineq1  42428  aks4d1p3  42448  aks4d1p5  42450  aks4d1p6  42451  aks4d1p8d1  42454  aks4d1p8d2  42455  aks4d1p8d3  42456  aks4d1p8  42457  aks4d1p9  42458  posbezout  42470  primrootscoprbij  42472  remexz  42474  primrootspoweq0  42476  aks6d1c1  42486  aks6d1c2p2  42489  hashscontpow1  42491  hashscontpow  42492  aks6d1c3  42493  aks6d1c4  42494  aks6d1c2lem4  42497  aks6d1c2  42500  aks6d1c5lem1  42506  sticksstones6  42521  sticksstones10  42525  sticksstones12a  42527  sticksstones12  42528  aks6d1c6lem3  42542  aks6d1c6lem4  42543  aks6d1c6isolem3  42546  aks6d1c6lem5  42547  aks6d1c7lem2  42551  aks6d1c7  42554  aks5lem1  42556  aks5lem2  42557  aks5lem3a  42559  grpods  42564  unitscyglem1  42565  unitscyglem2  42566  unitscyglem4  42568  unitscyglem5  42569  aks5  42574  sumcubes  42683  oexpreposd  42692  explt1d  42693  expeq1d  42694  expeqidd  42695  exp11d  42696  gcdle1d  42700  gcdle2d  42701  dvdsexpnn0  42704  fimgmcyc  42904  fltdvdsabdvdsc  42996  fltaccoprm  42998  fltbccoprm  42999  fltabcoprm  43000  fltne  43002  flt4lem2  43005  flt4lem3  43006  flt4lem4  43007  flt4lem5  43008  flt4lem5elem  43009  flt4lem5a  43010  flt4lem5b  43011  flt4lem5c  43012  flt4lem5d  43013  flt4lem5e  43014  flt4lem5f  43015  flt4lem6  43016  flt4lem7  43017  nna4b4nsq  43018  fltltc  43019  fltnlta  43021  irrapxlem3  43181  irrapxlem5  43183  pellexlem5  43190  pellexlem6  43191  pellex  43192  pell1234qrmulcl  43212  jm2.23  43353  jm2.20nn  43354  jm2.26lem3  43358  jm2.27a  43362  jm2.27b  43363  jm2.27c  43364  jm3.1lem1  43374  jm3.1lem3  43376  inductionexd  44511  nznngen  44672  hashnzfz2  44677  fmuldfeq  45943  divcnvg  45987  stoweidlem1  46359  stoweidlem3  46361  stoweidlem11  46369  stoweidlem20  46378  stoweidlem26  46384  stoweidlem34  46392  stoweidlem51  46409  stirlinglem4  46435  stirlinglem5  46436  stirlinglem8  46439  dirkerper  46454  dirkertrigeqlem2  46457  dirkertrigeqlem3  46458  dirkercncflem2  46462  fourierdlem11  46476  fourierdlem14  46479  fourierdlem20  46485  fourierdlem25  46490  fourierdlem37  46502  fourierdlem41  46506  fourierdlem48  46512  fourierdlem49  46513  fourierdlem54  46518  fourierdlem64  46528  fourierdlem73  46537  fourierdlem79  46543  fourierdlem92  46556  fourierdlem93  46557  fourierdlem111  46575  sqwvfourb  46587  etransclem3  46595  etransclem7  46599  etransclem10  46602  etransclem15  46607  etransclem24  46616  etransclem25  46617  etransclem26  46618  etransclem27  46619  etransclem28  46620  etransclem35  46627  etransclem37  46629  etransclem38  46630  etransclem41  46633  etransclem44  46636  etransclem45  46637  etransclem48  46640  ovnsubaddlem1  46928  vonioolem1  47038  iccpartgtprec  47780  iccpartipre  47781  fmtnoodd  47893  goldbachthlem2  47906  goldbachth  47907  odz2prm2pw  47923  fmtnoprmfac1lem  47924  fmtnoprmfac2lem1  47926  fmtnoprmfac2  47927  fmtnofac2lem  47928  2pwp1prm  47949  lighneallem1  47965  lighneallem4  47970  proththdlem  47973  proththd  47974  divgcdoddALTV  48042  perfectALTVlem1  48081  perfectALTVlem2  48082  perfectALTV  48083  gbowge7  48123  gpgedgvtx1  48422  gpg3kgrtriexlem2  48444  gpg3kgrtriexlem5  48447  pw2m1lepw2m1  48880  nnolog2flm1  48950  dignn0fr  48961  dignn0flhalflem1  48975