Theorem nnzd 12641

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

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

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 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7736  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-i2m1 11192  ax-1ne0 11193  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  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 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7416  df-om 7863  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-neg 11468  df-nn 12258  df-n0 12529  df-z 12616

This theorem is used by:  expaddzlem  14169  expmulz  14172  expmulnbnd  14299  facndiv  14352  bcval5  14382  bcpasc  14385  hashf1  14522  isercolllem1  15752  isercolllem2  15753  o1fsum  15900  bcxmas  15924  climcndslem2  15939  climcnds  15940  mertenslem1  15973  fprodser  16036  bpolydiflem  16140  eftlub  16197  eirrlem  16292  rpnnen2lem7  16308  rpnnen2lem9  16310  rpnnen2lem11  16312  sqrt2irrlem  16336  dvdsfac  16416  dvdsmod  16419  oddpwp1fsum  16482  bitsfzolem  16524  bitsmod  16526  bitsfi  16527  bitscmp  16528  bitsinv1  16532  sadadd3  16551  sadaddlem  16556  bitsuz  16564  bitsshft  16565  gcdnncl  16597  gcd1  16618  dvdsgcdidd  16627  bezoutlem3  16631  bezoutlem4  16632  mulgcd  16638  rplpwr  16648  rprpwr  16649  sqgcd  16652  expgcd  16653  nn0expgcd  16654  dvdssq  16657  lcmneg  16693  lcmgcdlem  16696  rpdvds  16750  coprmprod  16751  coprmproddvdslem  16752  congr  16754  cncongr1  16757  cncongr2  16758  prmz  16765  prmind2  16775  divgcdodd  16801  isprm6  16805  prmexpb  16810  prmfac1  16811  rpexp  16813  prmdvdsbc  16817  prmdvdsncoprmbd  16818  numdensq  16845  numdenexp  16851  hashdvds  16866  phiprmpw  16867  crth  16869  phimullem  16870  eulerthlem1  16872  eulerthlem2  16873  prmdivdiv  16878  hashgcdlem  16879  odzdvds  16887  pythagtriplem4  16911  pythagtriplem6  16913  pythagtriplem7  16914  pythagtriplem11  16917  pythagtriplem13  16919  pythagtriplem19  16925  pclem  16930  pcprendvds2  16933  pcpre1  16934  pcpremul  16935  pceulem  16937  pcqmul  16945  pcdvdsb  16961  pcidlem  16964  pcdvdstr  16968  pcgcd1  16969  pc2dvds  16971  pcprmpw2  16974  pcaddlem  16980  pcadd  16981  pcmpt2  16985  pcmptdvds  16986  pcfac  16991  pcbc  16992  qexpz  16993  oddprmdvds  16995  prmpwdvds  16996  pockthlem  16997  pockthg  16998  prmreclem2  17009  prmreclem3  17010  prmreclem4  17011  prmreclem5  17012  prmreclem6  17013  4sqlem5  17034  4sqlem8  17037  4sqlem9  17038  4sqlem10  17039  4sqlem12  17048  4sqlem14  17050  4sqlem16  17052  4sqlem17  17053  vdwlem1  17073  vdwlem2  17074  vdwlem3  17075  vdwlem6  17078  vdwlem9  17081  vdwlem10  17082  vdwnnlem3  17089  prmdvdsprmop  17135  prmolelcmf  17140  prmgaplem1  17141  prmgaplem7  17149  prmgaplem8  17150  gsumwsubmcl  18946  gsumsgrpccat  18949  gsumwmhm  18954  mulgneg  19215  mulgnndir  19226  psgnunilem4  19624  odlem2  19666  mndodconglem  19668  odmod  19673  gexlem2  19709  gexcl3  19714  gexcl2  19716  sylow1lem1  19725  sylow1lem3  19727  sylow1lem5  19729  pgpfi  19732  fislw  19752  sylow3lem4  19757  gexexlem  19979  ablfacrplem  20194  ablfacrp  20195  ablfacrp2  20196  ablfac1lem  20197  ablfac1b  20199  ablfac1eu  20202  pgpfac1lem3a  20205  ablfaclem3  20216  fincygsubgd  20240  fincygsubgodd  20241  znrrg  21778  psdpw  22398  cayhamlem1  23091  caublcls  25537  ovolicc2lem4  25748  iundisj2  25777  volsup  25784  uniioombllem3  25813  mbfi1fseqlem3  25945  mbfi1fseqlem4  25946  elqaalem2  26552  aalioulem1  26568  aalioulem4  26571  aalioulem5  26572  aalioulem6  26573  aaliou  26574  aaliou3lem1  26578  aaliou3lem2  26579  aaliou3lem3  26580  aaliou3lem8  26581  aaliou3lem5  26583  aaliou3lem6  26584  aaliou3lem7  26585  taylthlem2  26610  cxpeq  26994  zrtelqelz  26995  amgmlem  27226  lgamgulmlem4  27268  lgamcvg2  27291  wilthlem2  27305  wilth  27307  wilthimp  27308  ftalem5  27313  basellem2  27318  basellem3  27319  basellem4  27320  basellem5  27321  muval1  27369  dvdssqf  27374  sgmnncl  27383  efchtdvds  27395  mumullem2  27416  mumul  27417  sqff1o  27418  fsumdvdsdiaglem  27419  dvdsppwf1o  27422  dvdsflf1o  27423  muinv  27429  mpodvdsmulf1o  27430  dvdsmulf1o  27432  chtublem  27447  fsumvma2  27450  vmasum  27452  chpchtsum  27455  logfacubnd  27457  mersenne  27463  perfect1  27464  perfectlem1  27465  perfectlem2  27466  perfect  27467  dchrelbas4  27479  dchrfi  27491  bcmono  27513  bcp1ctr  27515  bclbnd  27516  bposlem1  27520  bposlem3  27522  bposlem5  27524  bposlem6  27525  bposlem9  27528  lgsmod  27559  lgsdir  27568  lgsdilem2  27569  lgsne0  27571  lgsqrlem2  27583  lgsqr  27587  lgsqrmodndvds  27589  gausslemma2dlem0c  27594  gausslemma2dlem0h  27599  gausslemma2dlem0i  27600  gausslemma2dlem2  27603  gausslemma2dlem6  27608  gausslemma2dlem7  27609  gausslemma2d  27610  lgseisenlem1  27611  lgseisenlem2  27612  lgseisenlem3  27613  lgseisenlem4  27614  lgsquadlem1  27616  lgsquadlem2  27617  lgsquadlem3  27618  lgsquad2lem1  27620  lgsquad2lem2  27621  lgsquad2  27622  m1lgs  27624  2lgslem2  27631  2sqlem3  27656  2sqlem4  27657  2sqlem8  27662  chebbnd1lem1  27705  rplogsumlem2  27721  rpvmasumlem  27723  dchrisumlem1  27725  dchrisumlem2  27726  dchrisumlem3  27727  dchrisum0fmul  27742  dchrisum0ff  27743  dchrisum0flblem1  27744  dchrisum0flblem2  27745  dchrisum0flb  27746  dchrisum0  27756  pntrsumbnd2  27803  pntrlog2bndlem1  27813  pntrlog2bndlem6  27819  pntpbnd2  27823  pntlemg  27834  pntlemj  27839  pntlemf  27841  ostth2lem2  27870  ostth2lem3  27871  ostth3  27874  numclwlk2lem2f1o  30859  nrt2irr  30953  minvecolem4  31361  iundisj2f  33063  ssnnssfz  33258  iundisj2fi  33268  f1ocnt  33271  elq2  33282  numdenneg  33285  expgt0b  33287  ltesubnnd  33293  oexpled  33306  psgnfzto1stlem  33540  isarchi3  33627  archiabllem1b  33632  zringfrac  33964  fldextrspundgdvds  34191  cos9thpiminplylem2  34293  smatrcl  34306  1smat1  34314  submateqlem1  34317  lmatfvlem  34325  qqhval2  34492  qqhf  34496  qqhghm  34498  qqhrhm  34499  qqhnm  34500  qqhre  34530  esumcvg  34596  meascnbl  34730  omssubadd  34811  oddpwdc  34865  ballotlemfp1  35003  ballotlemfc0  35004  ballotlemfcc  35005  ballotlemimin  35017  ballotlemic  35018  ballotlem1c  35019  hgt750lemc  35155  hgt750lemd  35156  hgt750lemb  35164  hgt750leme  35166  subfaclim  35767  cvmliftlem7  35870  sinccvglem  36251  bcprod  36317  bccolsum  36318  faclimlem2  36323  faclim2  36327  poimirlem1  38370  poimirlem2  38371  poimirlem3  38372  poimirlem4  38373  poimirlem6  38375  poimirlem8  38377  poimirlem9  38378  poimirlem10  38379  poimirlem11  38380  poimirlem13  38382  poimirlem14  38383  poimirlem15  38384  poimirlem16  38385  poimirlem17  38386  poimirlem18  38387  poimirlem19  38388  poimirlem20  38389  poimirlem21  38390  poimirlem22  38391  poimirlem23  38392  poimirlem24  38393  poimirlem26  38395  poimirlem27  38396  poimirlem28  38397  poimirlem31  38400  mblfinlem2  38407  seqpo  38497  incsequz  38498  incsequz2  38499  zndvdchrrhm  42839  bccl2d  42857  nnproddivdvdsd  42866  lcmineqlem1  42895  lcmineqlem3  42897  lcmineqlem4  42898  lcmineqlem6  42900  lcmineqlem8  42902  lcmineqlem9  42903  lcmineqlem10  42904  lcmineqlem11  42905  lcmineqlem13  42907  lcmineqlem14  42908  lcmineqlem18  42912  lcmineqlem19  42913  lcmineqlem20  42914  lcmineqlem21  42915  lcmineqlem22  42916  lcmineqlem23  42917  lcmineqlem  42918  3lexlogpow5ineq2  42921  3lexlogpow2ineq1  42924  aks4d1p3  42944  aks4d1p5  42946  aks4d1p6  42947  aks4d1p8d1  42950  aks4d1p8d2  42951  aks4d1p8d3  42952  aks4d1p8  42953  aks4d1p9  42954  posbezout  42966  primrootscoprbij  42968  remexz  42970  primrootspoweq0  42972  aks6d1c1  42982  aks6d1c2p2  42985  hashscontpow1  42987  hashscontpow  42988  aks6d1c3  42989  aks6d1c4  42990  aks6d1c2lem4  42993  aks6d1c2  42996  aks6d1c5lem1  43002  sticksstones6  43017  sticksstones10  43021  sticksstones12a  43023  sticksstones12  43024  aks6d1c6lem3  43038  aks6d1c6lem4  43039  aks6d1c6isolem3  43042  aks6d1c6lem5  43043  aks6d1c7lem2  43047  aks6d1c7  43050  aks5lem1  43052  aks5lem2  43053  aks5lem3a  43055  grpods  43060  unitscyglem1  43061  unitscyglem2  43062  unitscyglem4  43064  unitscyglem5  43065  aks5  43070  sumcubes  43188  oexpreposd  43197  explt1d  43198  expeq1d  43199  expeqidd  43200  exp11d  43201  gcdle1d  43205  gcdle2d  43206  dvdsexpnn0  43209  fimgmcyc  43416  fltdvdsabdvdsc  43484  fltaccoprm  43486  fltbccoprm  43487  fltabcoprm  43488  fltne  43490  flt4lem2  43493  flt4lem3  43494  flt4lem4  43495  flt4lem5  43496  flt4lem5elem  43497  flt4lem5a  43498  flt4lem5b  43499  flt4lem5c  43500  flt4lem5d  43501  flt4lem5e  43502  flt4lem5f  43503  flt4lem6  43504  flt4lem7  43505  nna4b4nsq  43506  fltltc  43507  fltnlta  43509  irrapxlem3  43665  irrapxlem5  43667  pellexlem5  43674  pellexlem6  43675  pellex  43676  pell1234qrmulcl  43696  jm2.23  43837  jm2.20nn  43838  jm2.26lem3  43842  jm2.27a  43846  jm2.27b  43847  jm2.27c  43848  jm3.1lem1  43858  jm3.1lem3  43860  inductionexd  44995  nznngen  45140  hashnzfz2  45145  fmuldfeq  46413  divcnvg  46457  stoweidlem1  46829  stoweidlem3  46831  stoweidlem11  46839  stoweidlem20  46848  stoweidlem26  46854  stoweidlem34  46862  stoweidlem51  46879  stirlinglem4  46905  stirlinglem5  46906  stirlinglem8  46909  dirkerper  46924  dirkertrigeqlem2  46927  dirkertrigeqlem3  46928  dirkercncflem2  46932  fourierdlem11  46946  fourierdlem14  46949  fourierdlem20  46955  fourierdlem25  46960  fourierdlem37  46972  fourierdlem41  46976  fourierdlem48  46982  fourierdlem49  46983  fourierdlem54  46988  fourierdlem64  46998  fourierdlem73  47007  fourierdlem79  47013  fourierdlem92  47026  fourierdlem93  47027  fourierdlem111  47045  sqwvfourb  47057  etransclem3  47065  etransclem7  47069  etransclem10  47072  etransclem15  47077  etransclem24  47086  etransclem25  47087  etransclem26  47088  etransclem27  47089  etransclem28  47090  etransclem35  47097  etransclem37  47099  etransclem38  47100  etransclem41  47103  etransclem44  47106  etransclem45  47107  etransclem48  47110  ovnsubaddlem1  47398  vonioolem1  47508  facnn0dvdsfac  48273  muldvdsfacgt  48274  muldvdsfacm1  48275  iccpartgtprec  48320  iccpartipre  48321  fmtnoodd  48436  goldbachthlem2  48449  goldbachth  48450  odz2prm2pw  48466  fmtnoprmfac1lem  48467  fmtnoprmfac2lem1  48469  fmtnoprmfac2  48470  fmtnofac2lem  48471  2pwp1prm  48492  lighneallem1  48508  lighneallem4  48513  proththdlem  48516  proththd  48517  nprmdvdsfacm1lem4  48526  ppivalnnprm  48528  ppivalnnnprmge6  48529  divgcdoddALTV  48598  perfectALTVlem1  48637  perfectALTVlem2  48638  perfectALTV  48639  gbowge7  48679  gpgedgvtx1  48978  gpg3kgrtriexlem2  49000  gpg3kgrtriexlem5  49003  pw2m1lepw2m1  49450  nnolog2flm1  49520  dignn0fr  49531  dignn0flhalflem1  49545