Theorem nnzd 12623

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

Syntax hints:   → wi 4   ∈ wcel 2098  ℕcn 12250  ℤcz 12596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429  ax-un 7741  ax-1cn 11203  ax-icn 11204  ax-addcl 11205  ax-addrcl 11206  ax-mulcl 11207  ax-mulrcl 11208  ax-i2m1 11213  ax-1ne0 11214  ax-rnegex 11216  ax-rrecex 11217  ax-cnre 11218

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-om 7872  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-neg 11484  df-nn 12251  df-n0 12511  df-z 12597

This theorem is referenced by:  expaddzlem  14111  expmulz  14114  expmulnbnd  14238  facndiv  14288  bcval5  14318  bcpasc  14321  hashf1  14459  isercolllem1  15652  isercolllem2  15653  o1fsum  15800  bcxmas  15822  climcndslem2  15837  climcnds  15838  mertenslem1  15871  fprodser  15934  bpolydiflem  16039  eftlub  16094  eirrlem  16189  rpnnen2lem7  16205  rpnnen2lem9  16207  rpnnen2lem11  16209  sqrt2irrlem  16233  dvdsfac  16311  dvdsmod  16314  oddpwp1fsum  16377  bitsfzolem  16417  bitsmod  16419  bitsfi  16420  bitscmp  16421  bitsinv1  16425  sadadd3  16444  sadaddlem  16449  bitsuz  16457  bitsshft  16458  gcdnncl  16490  gcd1  16511  dvdsgcdidd  16521  bezoutlem3  16525  bezoutlem4  16526  mulgcd  16532  rplpwr  16541  rprpwr  16542  sqgcd  16544  dvdssq  16546  lcmneg  16582  lcmgcdlem  16585  rpdvds  16639  coprmprod  16640  coprmproddvdslem  16641  congr  16643  cncongr1  16646  cncongr2  16647  prmz  16654  prmind2  16664  divgcdodd  16689  isprm6  16693  prmexpb  16699  prmfac1  16700  rpexp  16702  prmdvdsbc  16706  prmdvdsncoprmbd  16707  numdensq  16734  hashdvds  16752  phiprmpw  16753  crth  16755  phimullem  16756  eulerthlem1  16758  eulerthlem2  16759  prmdivdiv  16764  hashgcdlem  16765  odzdvds  16772  pythagtriplem4  16796  pythagtriplem6  16798  pythagtriplem7  16799  pythagtriplem11  16802  pythagtriplem13  16804  pythagtriplem19  16810  pclem  16815  pcprendvds2  16818  pcpre1  16819  pcpremul  16820  pceulem  16822  pcqmul  16830  pcdvdsb  16846  pcidlem  16849  pcdvdstr  16853  pcgcd1  16854  pc2dvds  16856  pcprmpw2  16859  pcaddlem  16865  pcadd  16866  pcmpt2  16870  pcmptdvds  16871  pcfac  16876  pcbc  16877  qexpz  16878  oddprmdvds  16880  prmpwdvds  16881  pockthlem  16882  pockthg  16883  prmreclem2  16894  prmreclem3  16895  prmreclem4  16896  prmreclem5  16897  prmreclem6  16898  4sqlem5  16919  4sqlem8  16922  4sqlem9  16923  4sqlem10  16924  4sqlem12  16933  4sqlem14  16935  4sqlem16  16937  4sqlem17  16938  vdwlem1  16958  vdwlem2  16959  vdwlem3  16960  vdwlem6  16963  vdwlem9  16966  vdwlem10  16967  vdwnnlem3  16974  prmdvdsprmop  17020  prmolelcmf  17025  prmgaplem1  17026  prmgaplem7  17034  prmgaplem8  17035  gsumwsubmcl  18802  gsumsgrpccat  18805  gsumwmhm  18810  mulgneg  19060  mulgnndir  19071  psgnunilem4  19469  odlem2  19511  mndodconglem  19513  odmod  19518  gexlem2  19554  gexcl3  19559  gexcl2  19561  sylow1lem1  19570  sylow1lem3  19572  sylow1lem5  19574  pgpfi  19577  fislw  19597  sylow3lem4  19602  gexexlem  19824  ablfacrplem  20039  ablfacrp  20040  ablfacrp2  20041  ablfac1lem  20042  ablfac1b  20044  ablfac1eu  20047  pgpfac1lem3a  20050  ablfaclem3  20061  fincygsubgd  20085  fincygsubgodd  20086  znrrg  21521  cayhamlem1  22817  caublcls  25286  ovolicc2lem4  25498  iundisj2  25527  volsup  25534  uniioombllem3  25563  mbfi1fseqlem3  25696  mbfi1fseqlem4  25697  elqaalem2  26305  aalioulem1  26317  aalioulem4  26320  aalioulem5  26321  aalioulem6  26322  aaliou  26323  aaliou3lem1  26327  aaliou3lem2  26328  aaliou3lem3  26329  aaliou3lem8  26330  aaliou3lem5  26332  aaliou3lem6  26333  aaliou3lem7  26334  taylthlem2  26359  taylthlem2OLD  26360  cxpeq  26742  amgmlem  26972  lgamgulmlem4  27014  lgamcvg2  27037  wilthlem2  27051  wilth  27053  wilthimp  27054  ftalem5  27059  basellem2  27064  basellem3  27065  basellem4  27066  basellem5  27067  muval1  27115  dvdssqf  27120  sgmnncl  27129  efchtdvds  27141  mumullem2  27162  mumul  27163  sqff1o  27164  fsumdvdsdiaglem  27165  dvdsppwf1o  27168  dvdsflf1o  27169  muinv  27175  mpodvdsmulf1o  27176  dvdsmulf1o  27178  chtublem  27194  fsumvma2  27197  vmasum  27199  chpchtsum  27202  logfacubnd  27204  mersenne  27210  perfect1  27211  perfectlem1  27212  perfectlem2  27213  perfect  27214  dchrelbas4  27226  dchrfi  27238  bcmono  27260  bcp1ctr  27262  bclbnd  27263  bposlem1  27267  bposlem3  27269  bposlem5  27271  bposlem6  27272  bposlem9  27275  lgsmod  27306  lgsdir  27315  lgsdilem2  27316  lgsne0  27318  lgsqrlem2  27330  lgsqr  27334  lgsqrmodndvds  27336  gausslemma2dlem0c  27341  gausslemma2dlem0h  27346  gausslemma2dlem0i  27347  gausslemma2dlem2  27350  gausslemma2dlem6  27355  gausslemma2dlem7  27356  gausslemma2d  27357  lgseisenlem1  27358  lgseisenlem2  27359  lgseisenlem3  27360  lgseisenlem4  27361  lgsquadlem1  27363  lgsquadlem2  27364  lgsquadlem3  27365  lgsquad2lem1  27367  lgsquad2lem2  27368  lgsquad2  27369  m1lgs  27371  2lgslem2  27378  2sqlem3  27403  2sqlem4  27404  2sqlem8  27409  chebbnd1lem1  27452  rplogsumlem2  27468  rpvmasumlem  27470  dchrisumlem1  27472  dchrisumlem2  27473  dchrisumlem3  27474  dchrisum0fmul  27489  dchrisum0ff  27490  dchrisum0flblem1  27491  dchrisum0flblem2  27492  dchrisum0flb  27493  dchrisum0  27503  pntrsumbnd2  27550  pntrlog2bndlem1  27560  pntrlog2bndlem6  27566  pntpbnd2  27570  pntlemg  27581  pntlemj  27586  pntlemf  27588  ostth2lem2  27617  ostth2lem3  27618  ostth3  27621  numclwlk2lem2f1o  30266  nrt2irr  30360  minvecolem4  30767  iundisj2f  32464  ssnnssfz  32642  iundisj2fi  32652  f1ocnt  32657  numdenneg  32668  ltesubnnd  32675  psgnfzto1stlem  32918  isarchi3  32992  archiabllem1b  32997  zringfrac  33371  smatrcl  33530  1smat1  33538  submateqlem1  33541  lmatfvlem  33549  qqhval2  33716  qqhf  33720  qqhghm  33722  qqhrhm  33723  qqhnm  33724  qqhre  33754  esumcvg  33838  meascnbl  33971  omssubadd  34053  oddpwdc  34107  ballotlemfp1  34244  ballotlemfc0  34245  ballotlemfcc  34246  ballotlemimin  34258  ballotlemic  34259  ballotlem1c  34260  hgt750lemc  34412  hgt750lemd  34413  hgt750lemb  34421  hgt750leme  34423  subfaclim  34931  cvmliftlem7  35034  sinccvglem  35409  bcprod  35465  bccolsum  35466  faclimlem2  35471  faclim2  35475  poimirlem1  37227  poimirlem2  37228  poimirlem3  37229  poimirlem4  37230  poimirlem6  37232  poimirlem8  37234  poimirlem9  37235  poimirlem10  37236  poimirlem11  37237  poimirlem13  37239  poimirlem14  37240  poimirlem15  37241  poimirlem16  37242  poimirlem17  37243  poimirlem18  37244  poimirlem19  37245  poimirlem20  37246  poimirlem21  37247  poimirlem22  37248  poimirlem23  37249  poimirlem24  37250  poimirlem26  37252  poimirlem27  37253  poimirlem28  37254  poimirlem31  37257  mblfinlem2  37264  seqpo  37353  incsequz  37354  incsequz2  37355  zndvdchrrhm  41575  bccl2d  41596  nnproddivdvdsd  41605  lcmineqlem1  41634  lcmineqlem3  41636  lcmineqlem4  41637  lcmineqlem6  41639  lcmineqlem8  41641  lcmineqlem9  41642  lcmineqlem10  41643  lcmineqlem11  41644  lcmineqlem13  41646  lcmineqlem14  41647  lcmineqlem18  41651  lcmineqlem19  41652  lcmineqlem20  41653  lcmineqlem21  41654  lcmineqlem22  41655  lcmineqlem23  41656  lcmineqlem  41657  3lexlogpow5ineq2  41660  3lexlogpow2ineq1  41663  aks4d1p3  41683  aks4d1p5  41685  aks4d1p6  41686  aks4d1p8d1  41689  aks4d1p8d2  41690  aks4d1p8d3  41691  aks4d1p8  41692  aks4d1p9  41693  posbezout  41705  primrootscoprbij  41707  remexz  41709  primrootspoweq0  41711  aks6d1c1  41721  aks6d1c2p2  41724  hashscontpow1  41726  hashscontpow  41727  aks6d1c3  41728  aks6d1c4  41729  aks6d1c2lem4  41732  aks6d1c2  41735  aks6d1c5lem1  41741  sticksstones6  41756  sticksstones10  41760  sticksstones12a  41762  sticksstones12  41763  aks6d1c6lem3  41777  aks6d1c6lem4  41778  aks6d1c6isolem3  41781  aks6d1c6lem5  41782  aks6d1c7lem2  41786  aks6d1c7  41789  aks5lem1  41791  aks5lem2  41792  metakunt1  41793  metakunt2  41794  metakunt3  41795  metakunt4  41796  metakunt5  41797  metakunt7  41799  metakunt10  41802  metakunt15  41807  metakunt16  41808  metakunt18  41810  metakunt19  41811  metakunt20  41812  metakunt21  41813  metakunt22  41814  metakunt24  41816  metakunt25  41817  metakunt26  41818  metakunt27  41819  metakunt28  41820  metakunt29  41821  metakunt30  41822  metakunt32  41824  metakunt33  41825  sumcubes  42010  oexpreposd  42018  exp11d  42022  gcdle1d  42027  gcdle2d  42028  expgcd  42031  nn0expgcd  42032  numdenexp  42034  dvdsexpnn0  42038  zrtelqelz  42041  fltdvdsabdvdsc  42199  fltaccoprm  42201  fltbccoprm  42202  fltabcoprm  42203  fltne  42205  flt4lem2  42208  flt4lem3  42209  flt4lem4  42210  flt4lem5  42211  flt4lem5elem  42212  flt4lem5a  42213  flt4lem5b  42214  flt4lem5c  42215  flt4lem5d  42216  flt4lem5e  42217  flt4lem5f  42218  flt4lem6  42219  flt4lem7  42220  nna4b4nsq  42221  fltltc  42222  fltnlta  42224  irrapxlem3  42388  irrapxlem5  42390  pellexlem5  42397  pellexlem6  42398  pellex  42399  pell1234qrmulcl  42419  jm2.23  42561  jm2.20nn  42562  jm2.26lem3  42566  jm2.27a  42570  jm2.27b  42571  jm2.27c  42572  jm3.1lem1  42582  jm3.1lem3  42584  inductionexd  43729  nznngen  43897  hashnzfz2  43902  fmuldfeq  45111  divcnvg  45155  stoweidlem1  45529  stoweidlem3  45531  stoweidlem11  45539  stoweidlem20  45548  stoweidlem26  45554  stoweidlem34  45562  stoweidlem51  45579  stirlinglem4  45605  stirlinglem5  45606  stirlinglem8  45609  dirkerper  45624  dirkertrigeqlem2  45627  dirkertrigeqlem3  45628  dirkercncflem2  45632  fourierdlem11  45646  fourierdlem14  45649  fourierdlem20  45655  fourierdlem25  45660  fourierdlem37  45672  fourierdlem41  45676  fourierdlem48  45682  fourierdlem49  45683  fourierdlem54  45688  fourierdlem64  45698  fourierdlem73  45707  fourierdlem79  45713  fourierdlem92  45726  fourierdlem93  45727  fourierdlem111  45745  sqwvfourb  45757  etransclem3  45765  etransclem7  45769  etransclem10  45772  etransclem15  45777  etransclem24  45786  etransclem25  45787  etransclem26  45788  etransclem27  45789  etransclem28  45790  etransclem35  45797  etransclem37  45799  etransclem38  45800  etransclem41  45803  etransclem44  45806  etransclem45  45807  etransclem48  45810  ovnsubaddlem1  46098  vonioolem1  46208  iccpartgtprec  46899  iccpartipre  46900  fmtnoodd  47012  goldbachthlem2  47025  goldbachth  47026  odz2prm2pw  47042  fmtnoprmfac1lem  47043  fmtnoprmfac2lem1  47045  fmtnoprmfac2  47046  fmtnofac2lem  47047  2pwp1prm  47068  lighneallem1  47084  lighneallem4  47089  proththdlem  47092  proththd  47093  divgcdoddALTV  47161  perfectALTVlem1  47200  perfectALTVlem2  47201  perfectALTV  47202  gbowge7  47242  pw2m1lepw2m1  47776  nnolog2flm1  47851  dignn0fr  47862  dignn0flhalflem1  47876