Theorem nnzd 12627

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℕcn 12243  ℤcz 12601

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5260  ax-nul 5272  ax-pr 5407  ax-un 7738  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-i2m1 11178  ax-1ne0 11179  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4876  df-iun 4961  df-br 5113  df-opab 5177  df-mpt 5196  df-tr 5222  df-id 5559  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7419  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-neg 11454  df-nn 12244  df-n0 12515  df-z 12602

This theorem is used by:  expaddzlem  14152  expmulz  14155  expmulnbnd  14282  facndiv  14335  bcval5  14365  bcpasc  14368  hashf1  14505  isercolllem1  15727  isercolllem2  15728  o1fsum  15876  bcxmas  15900  climcndslem2  15915  climcnds  15916  mertenslem1  15949  fprodser  16014  bpolydiflem  16118  eftlub  16175  eirrlem  16270  rpnnen2lem7  16286  rpnnen2lem9  16288  rpnnen2lem11  16290  sqrt2irrlem  16314  dvdsfac  16394  dvdsmod  16397  oddpwp1fsum  16460  bitsfzolem  16502  bitsmod  16504  bitsfi  16505  bitscmp  16506  bitsinv1  16510  sadadd3  16529  sadaddlem  16534  bitsuz  16542  bitsshft  16543  gcdnncl  16575  gcd1  16596  dvdsgcdidd  16605  bezoutlem3  16609  bezoutlem4  16610  mulgcd  16616  rplpwr  16626  rprpwr  16627  sqgcd  16630  expgcd  16631  nn0expgcd  16632  dvdssq  16635  lcmneg  16671  lcmgcdlem  16674  rpdvds  16728  coprmprod  16729  coprmproddvdslem  16730  congr  16732  cncongr1  16735  cncongr2  16736  prmz  16743  prmind2  16753  divgcdodd  16779  isprm6  16783  prmexpb  16788  prmfac1  16789  rpexp  16791  prmdvdsbc  16795  prmdvdsncoprmbd  16796  numdensq  16823  numdenexp  16829  hashdvds  16844  phiprmpw  16845  crth  16847  phimullem  16848  eulerthlem1  16850  eulerthlem2  16851  prmdivdiv  16856  hashgcdlem  16857  odzdvds  16865  pythagtriplem4  16889  pythagtriplem6  16891  pythagtriplem7  16892  pythagtriplem11  16895  pythagtriplem13  16897  pythagtriplem19  16903  pclem  16908  pcprendvds2  16911  pcpre1  16912  pcpremul  16913  pceulem  16915  pcqmul  16923  pcdvdsb  16939  pcidlem  16942  pcdvdstr  16946  pcgcd1  16947  pc2dvds  16949  pcprmpw2  16952  pcaddlem  16958  pcadd  16959  pcmpt2  16963  pcmptdvds  16964  pcfac  16969  pcbc  16970  qexpz  16971  oddprmdvds  16973  prmpwdvds  16974  pockthlem  16975  pockthg  16976  prmreclem2  16987  prmreclem3  16988  prmreclem4  16989  prmreclem5  16990  prmreclem6  16991  4sqlem5  17012  4sqlem8  17015  4sqlem9  17016  4sqlem10  17017  4sqlem12  17026  4sqlem14  17028  4sqlem16  17030  4sqlem17  17031  vdwlem1  17051  vdwlem2  17052  vdwlem3  17053  vdwlem6  17056  vdwlem9  17059  vdwlem10  17060  vdwnnlem3  17067  prmdvdsprmop  17113  prmolelcmf  17118  prmgaplem1  17119  prmgaplem7  17127  prmgaplem8  17128  gsumwsubmcl  18906  gsumsgrpccat  18909  gsumwmhm  18914  mulgneg  19168  mulgnndir  19179  psgnunilem4  19577  odlem2  19619  mndodconglem  19621  odmod  19626  gexlem2  19662  gexcl3  19667  gexcl2  19669  sylow1lem1  19678  sylow1lem3  19680  sylow1lem5  19682  pgpfi  19685  fislw  19705  sylow3lem4  19710  gexexlem  19932  ablfacrplem  20147  ablfacrp  20148  ablfacrp2  20149  ablfac1lem  20150  ablfac1b  20152  ablfac1eu  20155  pgpfac1lem3a  20158  ablfaclem3  20169  fincygsubgd  20193  fincygsubgodd  20194  znrrg  21730  psdpw  22348  cayhamlem1  23038  caublcls  25483  ovolicc2lem4  25694  iundisj2  25723  volsup  25730  uniioombllem3  25759  mbfi1fseqlem3  25891  mbfi1fseqlem4  25892  elqaalem2  26496  aalioulem1  26510  aalioulem4  26513  aalioulem5  26514  aalioulem6  26515  aaliou  26516  aaliou3lem1  26520  aaliou3lem2  26521  aaliou3lem3  26522  aaliou3lem8  26523  aaliou3lem5  26525  aaliou3lem6  26526  aaliou3lem7  26527  taylthlem2  26552  cxpeq  26937  zrtelqelz  26938  amgmlem  27169  lgamgulmlem4  27211  lgamcvg2  27234  wilthlem2  27248  wilth  27250  wilthimp  27251  ftalem5  27256  basellem2  27261  basellem3  27262  basellem4  27263  basellem5  27264  muval1  27312  dvdssqf  27317  sgmnncl  27326  efchtdvds  27338  mumullem2  27359  mumul  27360  sqff1o  27361  fsumdvdsdiaglem  27362  dvdsppwf1o  27365  dvdsflf1o  27366  muinv  27372  mpodvdsmulf1o  27373  dvdsmulf1o  27375  chtublem  27390  fsumvma2  27393  vmasum  27395  chpchtsum  27398  logfacubnd  27400  mersenne  27406  perfect1  27407  perfectlem1  27408  perfectlem2  27409  perfect  27410  dchrelbas4  27422  dchrfi  27434  bcmono  27456  bcp1ctr  27458  bclbnd  27459  bposlem1  27463  bposlem3  27465  bposlem5  27467  bposlem6  27468  bposlem9  27471  lgsmod  27502  lgsdir  27511  lgsdilem2  27512  lgsne0  27514  lgsqrlem2  27526  lgsqr  27530  lgsqrmodndvds  27532  gausslemma2dlem0c  27537  gausslemma2dlem0h  27542  gausslemma2dlem0i  27543  gausslemma2dlem2  27546  gausslemma2dlem6  27551  gausslemma2dlem7  27552  gausslemma2d  27553  lgseisenlem1  27554  lgseisenlem2  27555  lgseisenlem3  27556  lgseisenlem4  27557  lgsquadlem1  27559  lgsquadlem2  27560  lgsquadlem3  27561  lgsquad2lem1  27563  lgsquad2lem2  27564  lgsquad2  27565  m1lgs  27567  2lgslem2  27574  2sqlem3  27599  2sqlem4  27600  2sqlem8  27605  chebbnd1lem1  27648  rplogsumlem2  27664  rpvmasumlem  27666  dchrisumlem1  27668  dchrisumlem2  27669  dchrisumlem3  27670  dchrisum0fmul  27685  dchrisum0ff  27686  dchrisum0flblem1  27687  dchrisum0flblem2  27688  dchrisum0flb  27689  dchrisum0  27699  pntrsumbnd2  27746  pntrlog2bndlem1  27756  pntrlog2bndlem6  27762  pntpbnd2  27766  pntlemg  27777  pntlemj  27782  pntlemf  27784  ostth2lem2  27813  ostth2lem3  27814  ostth3  27817  numclwlk2lem2f1o  30745  nrt2irr  30839  minvecolem4  31247  iundisj2f  32950  ssnnssfz  33147  iundisj2fi  33157  f1ocnt  33160  elq2  33171  numdenneg  33174  expgt0b  33176  ltesubnnd  33182  oexpled  33195  psgnfzto1stlem  33433  isarchi3  33520  archiabllem1b  33525  zringfrac  33857  fldextrspundgdvds  34084  cos9thpiminplylem2  34186  smatrcl  34199  1smat1  34207  submateqlem1  34210  lmatfvlem  34218  qqhval2  34385  qqhf  34389  qqhghm  34391  qqhrhm  34392  qqhnm  34393  qqhre  34423  esumcvg  34489  meascnbl  34622  omssubadd  34703  oddpwdc  34757  ballotlemfp1  34895  ballotlemfc0  34896  ballotlemfcc  34897  ballotlemimin  34909  ballotlemic  34910  ballotlem1c  34911  hgt750lemc  35047  hgt750lemd  35048  hgt750lemb  35056  hgt750leme  35058  subfaclim  35692  cvmliftlem7  35795  sinccvglem  36176  bcprod  36242  bccolsum  36243  faclimlem2  36248  faclim2  36252  poimirlem1  38304  poimirlem2  38305  poimirlem3  38306  poimirlem4  38307  poimirlem6  38309  poimirlem8  38311  poimirlem9  38312  poimirlem10  38313  poimirlem11  38314  poimirlem13  38316  poimirlem14  38317  poimirlem15  38318  poimirlem16  38319  poimirlem17  38320  poimirlem18  38321  poimirlem19  38322  poimirlem20  38323  poimirlem21  38324  poimirlem22  38325  poimirlem23  38326  poimirlem24  38327  poimirlem26  38329  poimirlem27  38330  poimirlem28  38331  poimirlem31  38334  mblfinlem2  38341  seqpo  38430  incsequz  38431  incsequz2  38432  zndvdchrrhm  42772  bccl2d  42790  nnproddivdvdsd  42799  lcmineqlem1  42828  lcmineqlem3  42830  lcmineqlem4  42831  lcmineqlem6  42833  lcmineqlem8  42835  lcmineqlem9  42836  lcmineqlem10  42837  lcmineqlem11  42838  lcmineqlem13  42840  lcmineqlem14  42841  lcmineqlem18  42845  lcmineqlem19  42846  lcmineqlem20  42847  lcmineqlem21  42848  lcmineqlem22  42849  lcmineqlem23  42850  lcmineqlem  42851  3lexlogpow5ineq2  42854  3lexlogpow2ineq1  42857  aks4d1p3  42877  aks4d1p5  42879  aks4d1p6  42880  aks4d1p8d1  42883  aks4d1p8d2  42884  aks4d1p8d3  42885  aks4d1p8  42886  aks4d1p9  42887  posbezout  42899  primrootscoprbij  42901  remexz  42903  primrootspoweq0  42905  aks6d1c1  42915  aks6d1c2p2  42918  hashscontpow1  42920  hashscontpow  42921  aks6d1c3  42922  aks6d1c4  42923  aks6d1c2lem4  42926  aks6d1c2  42929  aks6d1c5lem1  42935  sticksstones6  42950  sticksstones10  42954  sticksstones12a  42956  sticksstones12  42957  aks6d1c6lem3  42971  aks6d1c6lem4  42972  aks6d1c6isolem3  42975  aks6d1c6lem5  42976  aks6d1c7lem2  42980  aks6d1c7  42983  aks5lem1  42985  aks5lem2  42986  aks5lem3a  42988  grpods  42993  unitscyglem1  42994  unitscyglem2  42995  unitscyglem4  42997  unitscyglem5  42998  aks5  43003  sumcubes  43106  oexpreposd  43115  explt1d  43116  expeq1d  43117  expeqidd  43118  exp11d  43119  gcdle1d  43123  gcdle2d  43124  dvdsexpnn0  43127  fimgmcyc  43334  fltdvdsabdvdsc  43402  fltaccoprm  43404  fltbccoprm  43405  fltabcoprm  43406  fltne  43408  flt4lem2  43411  flt4lem3  43412  flt4lem4  43413  flt4lem5  43414  flt4lem5elem  43415  flt4lem5a  43416  flt4lem5b  43417  flt4lem5c  43418  flt4lem5d  43419  flt4lem5e  43420  flt4lem5f  43421  flt4lem6  43422  flt4lem7  43423  nna4b4nsq  43424  fltltc  43425  fltnlta  43427  irrapxlem3  43583  irrapxlem5  43585  pellexlem5  43592  pellexlem6  43593  pellex  43594  pell1234qrmulcl  43614  jm2.23  43755  jm2.20nn  43756  jm2.26lem3  43760  jm2.27a  43764  jm2.27b  43765  jm2.27c  43766  jm3.1lem1  43776  jm3.1lem3  43778  inductionexd  44913  nznngen  45058  hashnzfz2  45063  fmuldfeq  46331  divcnvg  46375  stoweidlem1  46747  stoweidlem3  46749  stoweidlem11  46757  stoweidlem20  46766  stoweidlem26  46772  stoweidlem34  46780  stoweidlem51  46797  stirlinglem4  46823  stirlinglem5  46824  stirlinglem8  46827  dirkerper  46842  dirkertrigeqlem2  46845  dirkertrigeqlem3  46846  dirkercncflem2  46850  fourierdlem11  46864  fourierdlem14  46867  fourierdlem20  46873  fourierdlem25  46878  fourierdlem37  46890  fourierdlem41  46894  fourierdlem48  46900  fourierdlem49  46901  fourierdlem54  46906  fourierdlem64  46916  fourierdlem73  46925  fourierdlem79  46931  fourierdlem92  46944  fourierdlem93  46945  fourierdlem111  46963  sqwvfourb  46975  etransclem3  46983  etransclem7  46987  etransclem10  46990  etransclem15  46995  etransclem24  47004  etransclem25  47005  etransclem26  47006  etransclem27  47007  etransclem28  47008  etransclem35  47015  etransclem37  47017  etransclem38  47018  etransclem41  47021  etransclem44  47024  etransclem45  47025  etransclem48  47028  ovnsubaddlem1  47316  vonioolem1  47426  facnn0dvdsfac  48154  muldvdsfacgt  48155  muldvdsfacm1  48156  iccpartgtprec  48201  iccpartipre  48202  fmtnoodd  48317  goldbachthlem2  48330  goldbachth  48331  odz2prm2pw  48347  fmtnoprmfac1lem  48348  fmtnoprmfac2lem1  48350  fmtnoprmfac2  48351  fmtnofac2lem  48352  2pwp1prm  48373  lighneallem1  48389  lighneallem4  48394  proththdlem  48397  proththd  48398  nprmdvdsfacm1lem4  48407  ppivalnnprm  48409  ppivalnnnprmge6  48410  divgcdoddALTV  48479  perfectALTVlem1  48518  perfectALTVlem2  48519  perfectALTV  48520  gbowge7  48560  gpgedgvtx1  48859  gpg3kgrtriexlem2  48881  gpg3kgrtriexlem5  48884  pw2m1lepw2m1  49332  nnolog2flm1  49402  dignn0fr  49413  dignn0flhalflem1  49427