Theorem nnzd 12532

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℕcn 12162  ℤcz 12505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-i2m1 11112  ax-1ne0 11113  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-neg 11384  df-nn 12163  df-n0 12419  df-z 12506

This theorem is referenced by:  expaddzlem  14046  expmulz  14049  expmulnbnd  14176  facndiv  14229  bcval5  14259  bcpasc  14262  hashf1  14398  isercolllem1  15607  isercolllem2  15608  o1fsum  15755  bcxmas  15777  climcndslem2  15792  climcnds  15793  mertenslem1  15826  fprodser  15891  bpolydiflem  15996  eftlub  16053  eirrlem  16148  rpnnen2lem7  16164  rpnnen2lem9  16166  rpnnen2lem11  16168  sqrt2irrlem  16192  dvdsfac  16272  dvdsmod  16275  oddpwp1fsum  16338  bitsfzolem  16380  bitsmod  16382  bitsfi  16383  bitscmp  16384  bitsinv1  16388  sadadd3  16407  sadaddlem  16412  bitsuz  16420  bitsshft  16421  gcdnncl  16453  gcd1  16474  dvdsgcdidd  16483  bezoutlem3  16487  bezoutlem4  16488  mulgcd  16494  rplpwr  16504  rprpwr  16505  sqgcd  16508  expgcd  16509  nn0expgcd  16510  dvdssq  16513  lcmneg  16549  lcmgcdlem  16552  rpdvds  16606  coprmprod  16607  coprmproddvdslem  16608  congr  16610  cncongr1  16613  cncongr2  16614  prmz  16621  prmind2  16631  divgcdodd  16656  isprm6  16660  prmexpb  16665  prmfac1  16666  rpexp  16668  prmdvdsbc  16672  prmdvdsncoprmbd  16673  numdensq  16700  numdenexp  16706  hashdvds  16721  phiprmpw  16722  crth  16724  phimullem  16725  eulerthlem1  16727  eulerthlem2  16728  prmdivdiv  16733  hashgcdlem  16734  odzdvds  16742  pythagtriplem4  16766  pythagtriplem6  16768  pythagtriplem7  16769  pythagtriplem11  16772  pythagtriplem13  16774  pythagtriplem19  16780  pclem  16785  pcprendvds2  16788  pcpre1  16789  pcpremul  16790  pceulem  16792  pcqmul  16800  pcdvdsb  16816  pcidlem  16819  pcdvdstr  16823  pcgcd1  16824  pc2dvds  16826  pcprmpw2  16829  pcaddlem  16835  pcadd  16836  pcmpt2  16840  pcmptdvds  16841  pcfac  16846  pcbc  16847  qexpz  16848  oddprmdvds  16850  prmpwdvds  16851  pockthlem  16852  pockthg  16853  prmreclem2  16864  prmreclem3  16865  prmreclem4  16866  prmreclem5  16867  prmreclem6  16868  4sqlem5  16889  4sqlem8  16892  4sqlem9  16893  4sqlem10  16894  4sqlem12  16903  4sqlem14  16905  4sqlem16  16907  4sqlem17  16908  vdwlem1  16928  vdwlem2  16929  vdwlem3  16930  vdwlem6  16933  vdwlem9  16936  vdwlem10  16937  vdwnnlem3  16944  prmdvdsprmop  16990  prmolelcmf  16995  prmgaplem1  16996  prmgaplem7  17004  prmgaplem8  17005  gsumwsubmcl  18740  gsumsgrpccat  18743  gsumwmhm  18748  mulgneg  19000  mulgnndir  19011  psgnunilem4  19403  odlem2  19445  mndodconglem  19447  odmod  19452  gexlem2  19488  gexcl3  19493  gexcl2  19495  sylow1lem1  19504  sylow1lem3  19506  sylow1lem5  19508  pgpfi  19511  fislw  19531  sylow3lem4  19536  gexexlem  19758  ablfacrplem  19973  ablfacrp  19974  ablfacrp2  19975  ablfac1lem  19976  ablfac1b  19978  ablfac1eu  19981  pgpfac1lem3a  19984  ablfaclem3  19995  fincygsubgd  20019  fincygsubgodd  20020  znrrg  21451  psdpw  22033  cayhamlem1  22729  caublcls  25185  ovolicc2lem4  25397  iundisj2  25426  volsup  25433  uniioombllem3  25462  mbfi1fseqlem3  25594  mbfi1fseqlem4  25595  elqaalem2  26204  aalioulem1  26216  aalioulem4  26219  aalioulem5  26220  aalioulem6  26221  aaliou  26222  aaliou3lem1  26226  aaliou3lem2  26227  aaliou3lem3  26228  aaliou3lem8  26229  aaliou3lem5  26231  aaliou3lem6  26232  aaliou3lem7  26233  taylthlem2  26258  taylthlem2OLD  26259  cxpeq  26643  zrtelqelz  26644  amgmlem  26876  lgamgulmlem4  26918  lgamcvg2  26941  wilthlem2  26955  wilth  26957  wilthimp  26958  ftalem5  26963  basellem2  26968  basellem3  26969  basellem4  26970  basellem5  26971  muval1  27019  dvdssqf  27024  sgmnncl  27033  efchtdvds  27045  mumullem2  27066  mumul  27067  sqff1o  27068  fsumdvdsdiaglem  27069  dvdsppwf1o  27072  dvdsflf1o  27073  muinv  27079  mpodvdsmulf1o  27080  dvdsmulf1o  27082  chtublem  27098  fsumvma2  27101  vmasum  27103  chpchtsum  27106  logfacubnd  27108  mersenne  27114  perfect1  27115  perfectlem1  27116  perfectlem2  27117  perfect  27118  dchrelbas4  27130  dchrfi  27142  bcmono  27164  bcp1ctr  27166  bclbnd  27167  bposlem1  27171  bposlem3  27173  bposlem5  27175  bposlem6  27176  bposlem9  27179  lgsmod  27210  lgsdir  27219  lgsdilem2  27220  lgsne0  27222  lgsqrlem2  27234  lgsqr  27238  lgsqrmodndvds  27240  gausslemma2dlem0c  27245  gausslemma2dlem0h  27250  gausslemma2dlem0i  27251  gausslemma2dlem2  27254  gausslemma2dlem6  27259  gausslemma2dlem7  27260  gausslemma2d  27261  lgseisenlem1  27262  lgseisenlem2  27263  lgseisenlem3  27264  lgseisenlem4  27265  lgsquadlem1  27267  lgsquadlem2  27268  lgsquadlem3  27269  lgsquad2lem1  27271  lgsquad2lem2  27272  lgsquad2  27273  m1lgs  27275  2lgslem2  27282  2sqlem3  27307  2sqlem4  27308  2sqlem8  27313  chebbnd1lem1  27356  rplogsumlem2  27372  rpvmasumlem  27374  dchrisumlem1  27376  dchrisumlem2  27377  dchrisumlem3  27378  dchrisum0fmul  27393  dchrisum0ff  27394  dchrisum0flblem1  27395  dchrisum0flblem2  27396  dchrisum0flb  27397  dchrisum0  27407  pntrsumbnd2  27454  pntrlog2bndlem1  27464  pntrlog2bndlem6  27470  pntpbnd2  27474  pntlemg  27485  pntlemj  27490  pntlemf  27492  ostth2lem2  27521  ostth2lem3  27522  ostth3  27525  numclwlk2lem2f1o  30281  nrt2irr  30375  minvecolem4  30782  iundisj2f  32492  ssnnssfz  32683  iundisj2fi  32693  f1ocnt  32698  elq2  32709  numdenneg  32712  expgt0b  32714  ltesubnnd  32720  oexpled  32745  psgnfzto1stlem  33030  isarchi3  33114  archiabllem1b  33119  zringfrac  33498  fldextrspundgdvds  33649  cos9thpiminplylem2  33746  smatrcl  33759  1smat1  33767  submateqlem1  33770  lmatfvlem  33778  qqhval2  33945  qqhf  33949  qqhghm  33951  qqhrhm  33952  qqhnm  33953  qqhre  33983  esumcvg  34049  meascnbl  34182  omssubadd  34264  oddpwdc  34318  ballotlemfp1  34456  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemimin  34470  ballotlemic  34471  ballotlem1c  34472  hgt750lemc  34611  hgt750lemd  34612  hgt750lemb  34620  hgt750leme  34622  subfaclim  35148  cvmliftlem7  35251  sinccvglem  35632  bcprod  35698  bccolsum  35699  faclimlem2  35704  faclim2  35708  poimirlem1  37588  poimirlem2  37589  poimirlem3  37590  poimirlem4  37591  poimirlem6  37593  poimirlem8  37595  poimirlem9  37596  poimirlem10  37597  poimirlem11  37598  poimirlem13  37600  poimirlem14  37601  poimirlem15  37602  poimirlem16  37603  poimirlem17  37604  poimirlem18  37605  poimirlem19  37606  poimirlem20  37607  poimirlem21  37608  poimirlem22  37609  poimirlem23  37610  poimirlem24  37611  poimirlem26  37613  poimirlem27  37614  poimirlem28  37615  poimirlem31  37618  mblfinlem2  37625  seqpo  37714  incsequz  37715  incsequz2  37716  zndvdchrrhm  41933  bccl2d  41952  nnproddivdvdsd  41961  lcmineqlem1  41990  lcmineqlem3  41992  lcmineqlem4  41993  lcmineqlem6  41995  lcmineqlem8  41997  lcmineqlem9  41998  lcmineqlem10  41999  lcmineqlem11  42000  lcmineqlem13  42002  lcmineqlem14  42003  lcmineqlem18  42007  lcmineqlem19  42008  lcmineqlem20  42009  lcmineqlem21  42010  lcmineqlem22  42011  lcmineqlem23  42012  lcmineqlem  42013  3lexlogpow5ineq2  42016  3lexlogpow2ineq1  42019  aks4d1p3  42039  aks4d1p5  42041  aks4d1p6  42042  aks4d1p8d1  42045  aks4d1p8d2  42046  aks4d1p8d3  42047  aks4d1p8  42048  aks4d1p9  42049  posbezout  42061  primrootscoprbij  42063  remexz  42065  primrootspoweq0  42067  aks6d1c1  42077  aks6d1c2p2  42080  hashscontpow1  42082  hashscontpow  42083  aks6d1c3  42084  aks6d1c4  42085  aks6d1c2lem4  42088  aks6d1c2  42091  aks6d1c5lem1  42097  sticksstones6  42112  sticksstones10  42116  sticksstones12a  42118  sticksstones12  42119  aks6d1c6lem3  42133  aks6d1c6lem4  42134  aks6d1c6isolem3  42137  aks6d1c6lem5  42138  aks6d1c7lem2  42142  aks6d1c7  42145  aks5lem1  42147  aks5lem2  42148  aks5lem3a  42150  grpods  42155  unitscyglem1  42156  unitscyglem2  42157  unitscyglem4  42159  unitscyglem5  42160  aks5  42165  sumcubes  42274  oexpreposd  42283  explt1d  42284  expeq1d  42285  expeqidd  42286  exp11d  42287  gcdle1d  42291  gcdle2d  42292  dvdsexpnn0  42295  fimgmcyc  42495  fltdvdsabdvdsc  42599  fltaccoprm  42601  fltbccoprm  42602  fltabcoprm  42603  fltne  42605  flt4lem2  42608  flt4lem3  42609  flt4lem4  42610  flt4lem5  42611  flt4lem5elem  42612  flt4lem5a  42613  flt4lem5b  42614  flt4lem5c  42615  flt4lem5d  42616  flt4lem5e  42617  flt4lem5f  42618  flt4lem6  42619  flt4lem7  42620  nna4b4nsq  42621  fltltc  42622  fltnlta  42624  irrapxlem3  42785  irrapxlem5  42787  pellexlem5  42794  pellexlem6  42795  pellex  42796  pell1234qrmulcl  42816  jm2.23  42958  jm2.20nn  42959  jm2.26lem3  42963  jm2.27a  42967  jm2.27b  42968  jm2.27c  42969  jm3.1lem1  42979  jm3.1lem3  42981  inductionexd  44117  nznngen  44278  hashnzfz2  44283  fmuldfeq  45554  divcnvg  45598  stoweidlem1  45972  stoweidlem3  45974  stoweidlem11  45982  stoweidlem20  45991  stoweidlem26  45997  stoweidlem34  46005  stoweidlem51  46022  stirlinglem4  46048  stirlinglem5  46049  stirlinglem8  46052  dirkerper  46067  dirkertrigeqlem2  46070  dirkertrigeqlem3  46071  dirkercncflem2  46075  fourierdlem11  46089  fourierdlem14  46092  fourierdlem20  46098  fourierdlem25  46103  fourierdlem37  46115  fourierdlem41  46119  fourierdlem48  46125  fourierdlem49  46126  fourierdlem54  46131  fourierdlem64  46141  fourierdlem73  46150  fourierdlem79  46156  fourierdlem92  46169  fourierdlem93  46170  fourierdlem111  46188  sqwvfourb  46200  etransclem3  46208  etransclem7  46212  etransclem10  46215  etransclem15  46220  etransclem24  46229  etransclem25  46230  etransclem26  46231  etransclem27  46232  etransclem28  46233  etransclem35  46240  etransclem37  46242  etransclem38  46243  etransclem41  46246  etransclem44  46249  etransclem45  46250  etransclem48  46253  ovnsubaddlem1  46541  vonioolem1  46651  iccpartgtprec  47394  iccpartipre  47395  fmtnoodd  47507  goldbachthlem2  47520  goldbachth  47521  odz2prm2pw  47537  fmtnoprmfac1lem  47538  fmtnoprmfac2lem1  47540  fmtnoprmfac2  47541  fmtnofac2lem  47542  2pwp1prm  47563  lighneallem1  47579  lighneallem4  47584  proththdlem  47587  proththd  47588  divgcdoddALTV  47656  perfectALTVlem1  47695  perfectALTVlem2  47696  perfectALTV  47697  gbowge7  47737  gpgedgvtx1  48026  gpg3kgrtriexlem2  48048  gpg3kgrtriexlem5  48051  pw2m1lepw2m1  48482  nnolog2flm1  48552  dignn0fr  48563  dignn0flhalflem1  48577