Theorem nnzd 12712

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℕcn 12328  ℤcz 12686

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7749  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-i2m1 11261  ax-1ne0 11262  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7421  df-om 7876  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-neg 11537  df-nn 12329  df-n0 12600  df-z 12687

This theorem is used by:  expaddzlem  14241  expmulz  14244  expmulnbnd  14372  facndiv  14425  bcval5  14455  bcpasc  14458  hashf1  14595  isercolllem1  15825  isercolllem2  15826  o1fsum  15973  bcxmas  15997  climcndslem2  16012  climcnds  16013  mertenslem1  16046  fprodser  16109  bpolydiflem  16213  eftlub  16270  eirrlem  16365  rpnnen2lem7  16381  rpnnen2lem9  16383  rpnnen2lem11  16385  sqrt2irrlem  16409  dvdsfac  16489  dvdsmod  16492  oddpwp1fsum  16555  bitsfzolem  16597  bitsmod  16599  bitsfi  16600  bitscmp  16601  bitsinv1  16605  sadadd3  16624  sadaddlem  16629  bitsuz  16637  bitsshft  16638  gcdnncl  16670  gcdle1d  16673  gcdle2d  16674  gcd1  16694  dvdsgcdidd  16703  bezoutlem3  16707  bezoutlem4  16708  mulgcd  16714  rplpwr  16725  rprpwr  16726  sqgcd  16729  expgcd  16730  nn0expgcd  16731  dvdssq  16735  lcmneg  16771  lcmgcdlem  16774  rpdvds  16828  coprmprod  16829  coprmproddvdslem  16830  congr  16832  cncongr1  16835  cncongr2  16836  prmz  16843  prmind2  16853  divgcdodd  16879  isprm6  16883  prmexpb  16888  prmfac1  16889  rpexp  16891  prmdvdsbc  16895  prmdvdsncoprmbd  16896  numdensq  16923  numdenexp  16930  hashdvds  16945  phiprmpw  16946  crth  16948  phimullem  16949  eulerthlem1  16951  eulerthlem2  16952  prmdivdiv  16957  hashgcdlem  16958  odzdvds  16966  pythagtriplem4  16990  pythagtriplem6  16992  pythagtriplem7  16993  pythagtriplem11  16996  pythagtriplem13  16998  pythagtriplem19  17004  pclem  17009  pcprendvds2  17012  pcpre1  17013  pcpremul  17014  pceulem  17016  pcqmul  17024  pcdvdsb  17040  pcidlem  17043  pcdvdstr  17047  pcgcd1  17048  pc2dvds  17050  pcprmpw2  17053  pcaddlem  17059  pcadd  17060  pcmpt2  17064  pcmptdvds  17065  pcfac  17070  pcbc  17071  qexpz  17072  oddprmdvds  17074  prmpwdvds  17075  pockthlem  17076  pockthg  17077  prmreclem2  17088  prmreclem3  17089  prmreclem4  17090  prmreclem5  17091  prmreclem6  17092  4sqlem5  17113  4sqlem8  17116  4sqlem9  17117  4sqlem10  17118  4sqlem12  17127  4sqlem14  17129  4sqlem16  17131  4sqlem17  17132  vdwlem1  17152  vdwlem2  17153  vdwlem3  17154  vdwlem6  17157  vdwlem9  17160  vdwlem10  17161  vdwnnlem3  17168  prmdvdsprmop  17214  prmolelcmf  17219  prmgaplem1  17220  prmgaplem7  17228  prmgaplem8  17229  gsumwsubmcl  19026  gsumsgrpccat  19029  gsumwmhm  19034  mulgneg  19295  mulgnndir  19306  psgnunilem4  19704  odlem2  19746  mndodconglem  19748  odmod  19753  gexlem2  19789  gexcl3  19794  gexcl2  19796  sylow1lem1  19805  sylow1lem3  19807  sylow1lem5  19809  pgpfi  19812  fislw  19832  sylow3lem4  19837  gexexlem  20059  ablfacrplem  20274  ablfacrp  20275  ablfacrp2  20276  ablfac1lem  20277  ablfac1b  20279  ablfac1eu  20282  pgpfac1lem3a  20285  ablfaclem3  20296  fincygsubgd  20320  fincygsubgodd  20321  znrrg  21864  psdpw  22484  cayhamlem1  23177  caublcls  25623  ovolicc2lem4  25834  iundisj2  25863  volsup  25870  uniioombllem3  25899  mbfi1fseqlem3  26031  mbfi1fseqlem4  26032  elqaalem2  26636  aalioulem1  26652  aalioulem4  26655  aalioulem5  26656  aalioulem6  26657  aaliou  26658  aaliou3lem1  26662  aaliou3lem2  26663  aaliou3lem3  26664  aaliou3lem8  26665  aaliou3lem5  26667  aaliou3lem6  26668  aaliou3lem7  26669  taylthlem2  26694  cxpeq  27078  zrtelqelz  27079  amgmlem  27310  lgamgulmlem4  27352  lgamcvg2  27375  wilthlem2  27389  wilth  27391  wilthimp  27392  ftalem5  27397  basellem2  27402  basellem3  27403  basellem4  27404  basellem5  27405  muval1  27453  dvdssqf  27458  sgmnncl  27467  efchtdvds  27479  mumullem2  27500  mumul  27501  sqff1o  27502  fsumdvdsdiaglem  27503  dvdsppwf1o  27506  dvdsflf1o  27507  muinv  27513  mpodvdsmulf1o  27514  dvdsmulf1o  27516  chtublem  27531  fsumvma2  27534  vmasum  27536  chpchtsum  27539  logfacubnd  27541  mersenne  27547  perfect1  27548  perfectlem1  27549  perfectlem2  27550  perfect  27551  dchrelbas4  27563  dchrfi  27575  bcmono  27597  bcp1ctr  27599  bclbnd  27600  bposlem1  27604  bposlem3  27606  bposlem5  27608  bposlem6  27609  bposlem9  27612  lgsmod  27643  lgsdir  27652  lgsdilem2  27653  lgsne0  27655  lgsqrlem2  27667  lgsqr  27671  lgsqrmodndvds  27673  gausslemma2dlem0c  27678  gausslemma2dlem0h  27683  gausslemma2dlem0i  27684  gausslemma2dlem2  27687  gausslemma2dlem6  27692  gausslemma2dlem7  27693  gausslemma2d  27694  lgseisenlem1  27695  lgseisenlem2  27696  lgseisenlem3  27697  lgseisenlem4  27698  lgsquadlem1  27700  lgsquadlem2  27701  lgsquadlem3  27702  lgsquad2lem1  27704  lgsquad2lem2  27705  lgsquad2  27706  m1lgs  27708  2lgslem2  27715  2sqlem3  27740  2sqlem4  27741  2sqlem8  27746  chebbnd1lem1  27789  rplogsumlem2  27805  rpvmasumlem  27807  dchrisumlem1  27809  dchrisumlem2  27810  dchrisumlem3  27811  dchrisum0fmul  27826  dchrisum0ff  27827  dchrisum0flblem1  27828  dchrisum0flblem2  27829  dchrisum0flb  27830  dchrisum0  27840  pntrsumbnd2  27887  pntrlog2bndlem1  27897  pntrlog2bndlem6  27903  pntpbnd2  27907  pntlemg  27918  pntlemj  27923  pntlemf  27925  ostth2lem2  27954  ostth2lem3  27955  ostth3  27958  fltdvdsabdvdsc  27963  fltaccoprm  27965  fltbccoprm  27966  fltabcoprm  27967  fltne  27968  flt4lem2  27970  flt4lem3  27971  flt4lem4  27972  flt4lem5  27973  flt4lem5elem  27974  flt4lem5a  27975  flt4lem5b  27976  flt4lem5c  27977  flt4lem5d  27978  flt4lem5e  27979  flt4lem5f  27980  flt4lem6  27981  flt4lem7  27982  nna4b4nsq  27983  numclwlk2lem2f1o  30973  nrt2irr  31067  minvecolem4  31475  iundisj2f  33177  ssnnssfz  33372  iundisj2fi  33382  f1ocnt  33385  elq2  33396  numdenneg  33399  expgt0b  33401  ltesubnnd  33407  oexpled  33420  psgnfzto1stlem  33654  isarchi3  33741  archiabllem1b  33746  zringfrac  34079  fldextrspundgdvds  34306  cos9thpiminplylem2  34408  smatrcl  34421  1smat1  34429  submateqlem1  34432  lmatfvlem  34440  qqhval2  34607  qqhf  34611  qqhghm  34613  qqhrhm  34614  qqhnm  34615  qqhre  34645  esumcvg  34711  meascnbl  34845  omssubadd  34925  oddpwdc  34979  ballotlemfp1  35117  ballotlemfc0  35118  ballotlemfcc  35119  ballotlemimin  35131  ballotlemic  35132  ballotlem1c  35133  hgt750lemc  35269  hgt750lemd  35270  hgt750lemb  35278  hgt750leme  35280  subfaclim  35932  cvmliftlem7  36035  sinccvglem  36416  bcprod  36482  bccolsum  36483  faclimlem2  36488  faclim2  36492  poimirlem1  38519  poimirlem2  38520  poimirlem3  38521  poimirlem4  38522  poimirlem6  38524  poimirlem8  38526  poimirlem9  38527  poimirlem10  38528  poimirlem11  38529  poimirlem13  38531  poimirlem14  38532  poimirlem15  38533  poimirlem16  38534  poimirlem17  38535  poimirlem18  38536  poimirlem19  38537  poimirlem20  38538  poimirlem21  38539  poimirlem22  38540  poimirlem23  38541  poimirlem24  38542  poimirlem26  38544  poimirlem27  38545  poimirlem28  38546  poimirlem31  38549  mblfinlem2  38556  seqpo  38661  incsequz  38662  incsequz2  38663  zndvdchrrhm  43003  bccl2d  43021  nnproddivdvdsd  43030  lcmineqlem1  43059  lcmineqlem3  43061  lcmineqlem4  43062  lcmineqlem6  43064  lcmineqlem8  43066  lcmineqlem9  43067  lcmineqlem10  43068  lcmineqlem11  43069  lcmineqlem13  43071  lcmineqlem14  43072  lcmineqlem18  43076  lcmineqlem19  43077  lcmineqlem20  43078  lcmineqlem21  43079  lcmineqlem22  43080  lcmineqlem23  43081  lcmineqlem  43082  3lexlogpow5ineq2  43085  3lexlogpow2ineq1  43088  aks4d1p3  43108  aks4d1p5  43110  aks4d1p6  43111  aks4d1p8d1  43114  aks4d1p8d2  43115  aks4d1p8d3  43116  aks4d1p8  43117  aks4d1p9  43118  posbezout  43130  primrootscoprbij  43132  remexz  43134  primrootspoweq0  43136  aks6d1c1  43146  aks6d1c2p2  43149  hashscontpow1  43151  hashscontpow  43152  aks6d1c3  43153  aks6d1c4  43154  aks6d1c2lem4  43157  aks6d1c2  43160  aks6d1c5lem1  43166  sticksstones6  43181  sticksstones10  43185  sticksstones12a  43187  sticksstones12  43188  aks6d1c6lem3  43202  aks6d1c6lem4  43203  aks6d1c6isolem3  43206  aks6d1c6lem5  43207  aks6d1c7lem2  43211  aks6d1c7  43214  aks5lem1  43216  aks5lem2  43217  aks5lem3a  43219  grpods  43224  unitscyglem1  43225  unitscyglem2  43226  unitscyglem4  43228  unitscyglem5  43229  aks5  43234  sumcubes  43350  oexpreposd  43359  explt1d  43360  expeq1d  43361  expeqidd  43362  exp11d  43363  dvdsexpnn0  43366  fimgmcyc  43578  fltltc  43652  fltnlta  43654  irrapxlem3  43810  irrapxlem5  43812  pellexlem5  43819  pellexlem6  43820  pellex  43821  pell1234qrmulcl  43841  jm2.23  43982  jm2.20nn  43983  jm2.26lem3  43987  jm2.27a  43991  jm2.27b  43992  jm2.27c  43993  jm3.1lem1  44003  jm3.1lem3  44005  inductionexd  45140  nznngen  45285  hashnzfz2  45290  fmuldfeq  46564  divcnvg  46608  stoweidlem1  46980  stoweidlem3  46982  stoweidlem11  46990  stoweidlem20  46999  stoweidlem26  47005  stoweidlem34  47013  stoweidlem51  47030  stirlinglem4  47056  stirlinglem5  47057  stirlinglem8  47060  dirkerper  47075  dirkertrigeqlem2  47078  dirkertrigeqlem3  47079  dirkercncflem2  47083  fourierdlem11  47097  fourierdlem14  47100  fourierdlem20  47106  fourierdlem25  47111  fourierdlem37  47123  fourierdlem41  47127  fourierdlem48  47133  fourierdlem49  47134  fourierdlem54  47139  fourierdlem64  47149  fourierdlem73  47158  fourierdlem79  47164  fourierdlem92  47177  fourierdlem93  47178  fourierdlem111  47196  sqwvfourb  47208  etransclem3  47216  etransclem7  47220  etransclem10  47223  etransclem15  47228  etransclem24  47237  etransclem25  47238  etransclem26  47239  etransclem27  47240  etransclem28  47241  etransclem35  47248  etransclem37  47250  etransclem38  47251  etransclem41  47254  etransclem44  47257  etransclem45  47258  etransclem48  47261  ovnsubaddlem1  47549  vonioolem1  47659  facnn0dvdsfac  48424  muldvdsfacgt  48425  muldvdsfacm1  48426  iccpartgtprec  48471  iccpartipre  48472  fmtnoodd  48587  goldbachthlem2  48600  goldbachth  48601  odz2prm2pw  48617  fmtnoprmfac1lem  48618  fmtnoprmfac2lem1  48620  fmtnoprmfac2  48621  fmtnofac2lem  48622  2pwp1prm  48643  lighneallem1  48659  lighneallem4  48664  proththdlem  48667  proththd  48668  nprmdvdsfacm1lem4  48677  ppivalnnprm  48679  ppivalnnnprmge6  48680  divgcdoddALTV  48749  perfectALTVlem1  48788  perfectALTVlem2  48789  perfectALTV  48790  gbowge7  48830  gpgedgvtx1  49129  gpg3kgrtriexlem2  49151  gpg3kgrtriexlem5  49154  pw2m1lepw2m1  49601  nnolog2flm1  49671  dignn0fr  49682  dignn0flhalflem1  49696