Theorem nnzd 12628

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

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

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 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7738  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-addrcl 11172  ax-mulcl 11173  ax-mulrcl 11174  ax-i2m1 11179  ax-1ne0 11180  ax-rnegex 11182  ax-rrecex 11183  ax-cnre 11184

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  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 11455  df-nn 12245  df-n0 12516  df-z 12603

This theorem is used by:  expaddzlem  14155  expmulz  14158  expmulnbnd  14285  facndiv  14338  bcval5  14368  bcpasc  14371  hashf1  14508  isercolllem1  15736  isercolllem2  15737  o1fsum  15884  bcxmas  15908  climcndslem2  15923  climcnds  15924  mertenslem1  15957  fprodser  16022  bpolydiflem  16126  eftlub  16183  eirrlem  16278  rpnnen2lem7  16294  rpnnen2lem9  16296  rpnnen2lem11  16298  sqrt2irrlem  16322  dvdsfac  16402  dvdsmod  16405  oddpwp1fsum  16468  bitsfzolem  16510  bitsmod  16512  bitsfi  16513  bitscmp  16514  bitsinv1  16518  sadadd3  16537  sadaddlem  16542  bitsuz  16550  bitsshft  16551  gcdnncl  16583  gcd1  16604  dvdsgcdidd  16613  bezoutlem3  16617  bezoutlem4  16618  mulgcd  16624  rplpwr  16634  rprpwr  16635  sqgcd  16638  expgcd  16639  nn0expgcd  16640  dvdssq  16643  lcmneg  16679  lcmgcdlem  16682  rpdvds  16736  coprmprod  16737  coprmproddvdslem  16738  congr  16740  cncongr1  16743  cncongr2  16744  prmz  16751  prmind2  16761  divgcdodd  16787  isprm6  16791  prmexpb  16796  prmfac1  16797  rpexp  16799  prmdvdsbc  16803  prmdvdsncoprmbd  16804  numdensq  16831  numdenexp  16837  hashdvds  16852  phiprmpw  16853  crth  16855  phimullem  16856  eulerthlem1  16858  eulerthlem2  16859  prmdivdiv  16864  hashgcdlem  16865  odzdvds  16873  pythagtriplem4  16897  pythagtriplem6  16899  pythagtriplem7  16900  pythagtriplem11  16903  pythagtriplem13  16905  pythagtriplem19  16911  pclem  16916  pcprendvds2  16919  pcpre1  16920  pcpremul  16921  pceulem  16923  pcqmul  16931  pcdvdsb  16947  pcidlem  16950  pcdvdstr  16954  pcgcd1  16955  pc2dvds  16957  pcprmpw2  16960  pcaddlem  16966  pcadd  16967  pcmpt2  16971  pcmptdvds  16972  pcfac  16977  pcbc  16978  qexpz  16979  oddprmdvds  16981  prmpwdvds  16982  pockthlem  16983  pockthg  16984  prmreclem2  16995  prmreclem3  16996  prmreclem4  16997  prmreclem5  16998  prmreclem6  16999  4sqlem5  17020  4sqlem8  17023  4sqlem9  17024  4sqlem10  17025  4sqlem12  17034  4sqlem14  17036  4sqlem16  17038  4sqlem17  17039  vdwlem1  17059  vdwlem2  17060  vdwlem3  17061  vdwlem6  17064  vdwlem9  17067  vdwlem10  17068  vdwnnlem3  17075  prmdvdsprmop  17121  prmolelcmf  17126  prmgaplem1  17127  prmgaplem7  17135  prmgaplem8  17136  gsumwsubmcl  18920  gsumsgrpccat  18923  gsumwmhm  18928  mulgneg  19182  mulgnndir  19193  psgnunilem4  19591  odlem2  19633  mndodconglem  19635  odmod  19640  gexlem2  19676  gexcl3  19681  gexcl2  19683  sylow1lem1  19692  sylow1lem3  19694  sylow1lem5  19696  pgpfi  19699  fislw  19719  sylow3lem4  19724  gexexlem  19946  ablfacrplem  20161  ablfacrp  20162  ablfacrp2  20163  ablfac1lem  20164  ablfac1b  20166  ablfac1eu  20169  pgpfac1lem3a  20172  ablfaclem3  20183  fincygsubgd  20207  fincygsubgodd  20208  znrrg  21745  psdpw  22363  cayhamlem1  23053  caublcls  25499  ovolicc2lem4  25710  iundisj2  25739  volsup  25746  uniioombllem3  25775  mbfi1fseqlem3  25907  mbfi1fseqlem4  25908  elqaalem2  26512  aalioulem1  26526  aalioulem4  26529  aalioulem5  26530  aalioulem6  26531  aaliou  26532  aaliou3lem1  26536  aaliou3lem2  26537  aaliou3lem3  26538  aaliou3lem8  26539  aaliou3lem5  26541  aaliou3lem6  26542  aaliou3lem7  26543  taylthlem2  26568  cxpeq  26953  zrtelqelz  26954  amgmlem  27185  lgamgulmlem4  27227  lgamcvg2  27250  wilthlem2  27264  wilth  27266  wilthimp  27267  ftalem5  27272  basellem2  27277  basellem3  27278  basellem4  27279  basellem5  27280  muval1  27328  dvdssqf  27333  sgmnncl  27342  efchtdvds  27354  mumullem2  27375  mumul  27376  sqff1o  27377  fsumdvdsdiaglem  27378  dvdsppwf1o  27381  dvdsflf1o  27382  muinv  27388  mpodvdsmulf1o  27389  dvdsmulf1o  27391  chtublem  27406  fsumvma2  27409  vmasum  27411  chpchtsum  27414  logfacubnd  27416  mersenne  27422  perfect1  27423  perfectlem1  27424  perfectlem2  27425  perfect  27426  dchrelbas4  27438  dchrfi  27450  bcmono  27472  bcp1ctr  27474  bclbnd  27475  bposlem1  27479  bposlem3  27481  bposlem5  27483  bposlem6  27484  bposlem9  27487  lgsmod  27518  lgsdir  27527  lgsdilem2  27528  lgsne0  27530  lgsqrlem2  27542  lgsqr  27546  lgsqrmodndvds  27548  gausslemma2dlem0c  27553  gausslemma2dlem0h  27558  gausslemma2dlem0i  27559  gausslemma2dlem2  27562  gausslemma2dlem6  27567  gausslemma2dlem7  27568  gausslemma2d  27569  lgseisenlem1  27570  lgseisenlem2  27571  lgseisenlem3  27572  lgseisenlem4  27573  lgsquadlem1  27575  lgsquadlem2  27576  lgsquadlem3  27577  lgsquad2lem1  27579  lgsquad2lem2  27580  lgsquad2  27581  m1lgs  27583  2lgslem2  27590  2sqlem3  27615  2sqlem4  27616  2sqlem8  27621  chebbnd1lem1  27664  rplogsumlem2  27680  rpvmasumlem  27682  dchrisumlem1  27684  dchrisumlem2  27685  dchrisumlem3  27686  dchrisum0fmul  27701  dchrisum0ff  27702  dchrisum0flblem1  27703  dchrisum0flblem2  27704  dchrisum0flb  27705  dchrisum0  27715  pntrsumbnd2  27762  pntrlog2bndlem1  27772  pntrlog2bndlem6  27778  pntpbnd2  27782  pntlemg  27793  pntlemj  27798  pntlemf  27800  ostth2lem2  27829  ostth2lem3  27830  ostth3  27833  numclwlk2lem2f1o  30777  nrt2irr  30871  minvecolem4  31279  iundisj2f  32982  ssnnssfz  33178  iundisj2fi  33188  f1ocnt  33191  elq2  33202  numdenneg  33205  expgt0b  33207  ltesubnnd  33213  oexpled  33226  psgnfzto1stlem  33460  isarchi3  33547  archiabllem1b  33552  zringfrac  33884  fldextrspundgdvds  34111  cos9thpiminplylem2  34213  smatrcl  34226  1smat1  34234  submateqlem1  34237  lmatfvlem  34245  qqhval2  34412  qqhf  34416  qqhghm  34418  qqhrhm  34419  qqhnm  34420  qqhre  34450  esumcvg  34516  meascnbl  34650  omssubadd  34731  oddpwdc  34785  ballotlemfp1  34923  ballotlemfc0  34924  ballotlemfcc  34925  ballotlemimin  34937  ballotlemic  34938  ballotlem1c  34939  hgt750lemc  35075  hgt750lemd  35076  hgt750lemb  35084  hgt750leme  35086  subfaclim  35693  cvmliftlem7  35796  sinccvglem  36177  bcprod  36243  bccolsum  36244  faclimlem2  36249  faclim2  36253  poimirlem1  38305  poimirlem2  38306  poimirlem3  38307  poimirlem4  38308  poimirlem6  38310  poimirlem8  38312  poimirlem9  38313  poimirlem10  38314  poimirlem11  38315  poimirlem13  38317  poimirlem14  38318  poimirlem15  38319  poimirlem16  38320  poimirlem17  38321  poimirlem18  38322  poimirlem19  38323  poimirlem20  38324  poimirlem21  38325  poimirlem22  38326  poimirlem23  38327  poimirlem24  38328  poimirlem26  38330  poimirlem27  38331  poimirlem28  38332  poimirlem31  38335  mblfinlem2  38342  seqpo  38431  incsequz  38432  incsequz2  38433  zndvdchrrhm  42773  bccl2d  42791  nnproddivdvdsd  42800  lcmineqlem1  42829  lcmineqlem3  42831  lcmineqlem4  42832  lcmineqlem6  42834  lcmineqlem8  42836  lcmineqlem9  42837  lcmineqlem10  42838  lcmineqlem11  42839  lcmineqlem13  42841  lcmineqlem14  42842  lcmineqlem18  42846  lcmineqlem19  42847  lcmineqlem20  42848  lcmineqlem21  42849  lcmineqlem22  42850  lcmineqlem23  42851  lcmineqlem  42852  3lexlogpow5ineq2  42855  3lexlogpow2ineq1  42858  aks4d1p3  42878  aks4d1p5  42880  aks4d1p6  42881  aks4d1p8d1  42884  aks4d1p8d2  42885  aks4d1p8d3  42886  aks4d1p8  42887  aks4d1p9  42888  posbezout  42900  primrootscoprbij  42902  remexz  42904  primrootspoweq0  42906  aks6d1c1  42916  aks6d1c2p2  42919  hashscontpow1  42921  hashscontpow  42922  aks6d1c3  42923  aks6d1c4  42924  aks6d1c2lem4  42927  aks6d1c2  42930  aks6d1c5lem1  42936  sticksstones6  42951  sticksstones10  42955  sticksstones12a  42957  sticksstones12  42958  aks6d1c6lem3  42972  aks6d1c6lem4  42973  aks6d1c6isolem3  42976  aks6d1c6lem5  42977  aks6d1c7lem2  42981  aks6d1c7  42984  aks5lem1  42986  aks5lem2  42987  aks5lem3a  42989  grpods  42994  unitscyglem1  42995  unitscyglem2  42996  unitscyglem4  42998  unitscyglem5  42999  aks5  43004  sumcubes  43107  oexpreposd  43116  explt1d  43117  expeq1d  43118  expeqidd  43119  exp11d  43120  gcdle1d  43124  gcdle2d  43125  dvdsexpnn0  43128  fimgmcyc  43335  fltdvdsabdvdsc  43403  fltaccoprm  43405  fltbccoprm  43406  fltabcoprm  43407  fltne  43409  flt4lem2  43412  flt4lem3  43413  flt4lem4  43414  flt4lem5  43415  flt4lem5elem  43416  flt4lem5a  43417  flt4lem5b  43418  flt4lem5c  43419  flt4lem5d  43420  flt4lem5e  43421  flt4lem5f  43422  flt4lem6  43423  flt4lem7  43424  nna4b4nsq  43425  fltltc  43426  fltnlta  43428  irrapxlem3  43584  irrapxlem5  43586  pellexlem5  43593  pellexlem6  43594  pellex  43595  pell1234qrmulcl  43615  jm2.23  43756  jm2.20nn  43757  jm2.26lem3  43761  jm2.27a  43765  jm2.27b  43766  jm2.27c  43767  jm3.1lem1  43777  jm3.1lem3  43779  inductionexd  44914  nznngen  45059  hashnzfz2  45064  fmuldfeq  46332  divcnvg  46376  stoweidlem1  46748  stoweidlem3  46750  stoweidlem11  46758  stoweidlem20  46767  stoweidlem26  46773  stoweidlem34  46781  stoweidlem51  46798  stirlinglem4  46824  stirlinglem5  46825  stirlinglem8  46828  dirkerper  46843  dirkertrigeqlem2  46846  dirkertrigeqlem3  46847  dirkercncflem2  46851  fourierdlem11  46865  fourierdlem14  46868  fourierdlem20  46874  fourierdlem25  46879  fourierdlem37  46891  fourierdlem41  46895  fourierdlem48  46901  fourierdlem49  46902  fourierdlem54  46907  fourierdlem64  46917  fourierdlem73  46926  fourierdlem79  46932  fourierdlem92  46945  fourierdlem93  46946  fourierdlem111  46964  sqwvfourb  46976  etransclem3  46984  etransclem7  46988  etransclem10  46991  etransclem15  46996  etransclem24  47005  etransclem25  47006  etransclem26  47007  etransclem27  47008  etransclem28  47009  etransclem35  47016  etransclem37  47018  etransclem38  47019  etransclem41  47022  etransclem44  47025  etransclem45  47026  etransclem48  47029  ovnsubaddlem1  47317  vonioolem1  47427  facnn0dvdsfac  48155  muldvdsfacgt  48156  muldvdsfacm1  48157  iccpartgtprec  48202  iccpartipre  48203  fmtnoodd  48318  goldbachthlem2  48331  goldbachth  48332  odz2prm2pw  48348  fmtnoprmfac1lem  48349  fmtnoprmfac2lem1  48351  fmtnoprmfac2  48352  fmtnofac2lem  48353  2pwp1prm  48374  lighneallem1  48390  lighneallem4  48395  proththdlem  48398  proththd  48399  nprmdvdsfacm1lem4  48408  ppivalnnprm  48410  ppivalnnnprmge6  48411  divgcdoddALTV  48480  perfectALTVlem1  48519  perfectALTVlem2  48520  perfectALTV  48521  gbowge7  48561  gpgedgvtx1  48860  gpg3kgrtriexlem2  48882  gpg3kgrtriexlem5  48885  pw2m1lepw2m1  49333  nnolog2flm1  49403  dignn0fr  49414  dignn0flhalflem1  49428