Theorem nnzd 12613

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

Syntax hints:   → wi 4   ∈ wcel 2149  ℕcn 12229  ℤcz 12587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402  ax-un 7730  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-i2m1 11164  ax-1ne0 11165  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6300  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-ov 7411  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-neg 11440  df-nn 12230  df-n0 12501  df-z 12588

This theorem is referenced by:  expaddzlem  14137  expmulz  14140  expmulnbnd  14267  facndiv  14320  bcval5  14350  bcpasc  14353  hashf1  14490  isercolllem1  15712  isercolllem2  15713  o1fsum  15861  bcxmas  15885  climcndslem2  15900  climcnds  15901  mertenslem1  15934  fprodser  15999  bpolydiflem  16104  eftlub  16161  eirrlem  16256  rpnnen2lem7  16272  rpnnen2lem9  16274  rpnnen2lem11  16276  sqrt2irrlem  16300  dvdsfac  16380  dvdsmod  16383  oddpwp1fsum  16446  bitsfzolem  16488  bitsmod  16490  bitsfi  16491  bitscmp  16492  bitsinv1  16496  sadadd3  16515  sadaddlem  16520  bitsuz  16528  bitsshft  16529  gcdnncl  16561  gcd1  16582  dvdsgcdidd  16591  bezoutlem3  16595  bezoutlem4  16596  mulgcd  16602  rplpwr  16612  rprpwr  16613  sqgcd  16616  expgcd  16617  nn0expgcd  16618  dvdssq  16621  lcmneg  16657  lcmgcdlem  16660  rpdvds  16714  coprmprod  16715  coprmproddvdslem  16716  congr  16718  cncongr1  16721  cncongr2  16722  prmz  16729  prmind2  16739  divgcdodd  16765  isprm6  16769  prmexpb  16774  prmfac1  16775  rpexp  16777  prmdvdsbc  16781  prmdvdsncoprmbd  16782  numdensq  16809  numdenexp  16815  hashdvds  16830  phiprmpw  16831  crth  16833  phimullem  16834  eulerthlem1  16836  eulerthlem2  16837  prmdivdiv  16842  hashgcdlem  16843  odzdvds  16851  pythagtriplem4  16875  pythagtriplem6  16877  pythagtriplem7  16878  pythagtriplem11  16881  pythagtriplem13  16883  pythagtriplem19  16889  pclem  16894  pcprendvds2  16897  pcpre1  16898  pcpremul  16899  pceulem  16901  pcqmul  16909  pcdvdsb  16925  pcidlem  16928  pcdvdstr  16932  pcgcd1  16933  pc2dvds  16935  pcprmpw2  16938  pcaddlem  16944  pcadd  16945  pcmpt2  16949  pcmptdvds  16950  pcfac  16955  pcbc  16956  qexpz  16957  oddprmdvds  16959  prmpwdvds  16960  pockthlem  16961  pockthg  16962  prmreclem2  16973  prmreclem3  16974  prmreclem4  16975  prmreclem5  16976  prmreclem6  16977  4sqlem5  16998  4sqlem8  17001  4sqlem9  17002  4sqlem10  17003  4sqlem12  17012  4sqlem14  17014  4sqlem16  17016  4sqlem17  17017  vdwlem1  17037  vdwlem2  17038  vdwlem3  17039  vdwlem6  17042  vdwlem9  17045  vdwlem10  17046  vdwnnlem3  17053  prmdvdsprmop  17099  prmolelcmf  17104  prmgaplem1  17105  prmgaplem7  17113  prmgaplem8  17114  gsumwsubmcl  18892  gsumsgrpccat  18895  gsumwmhm  18900  mulgneg  19154  mulgnndir  19165  psgnunilem4  19563  odlem2  19605  mndodconglem  19607  odmod  19612  gexlem2  19648  gexcl3  19653  gexcl2  19655  sylow1lem1  19664  sylow1lem3  19666  sylow1lem5  19668  pgpfi  19671  fislw  19691  sylow3lem4  19696  gexexlem  19918  ablfacrplem  20133  ablfacrp  20134  ablfacrp2  20135  ablfac1lem  20136  ablfac1b  20138  ablfac1eu  20141  pgpfac1lem3a  20144  ablfaclem3  20155  fincygsubgd  20179  fincygsubgodd  20180  znrrg  21680  psdpw  22298  cayhamlem1  22988  caublcls  25433  ovolicc2lem4  25644  iundisj2  25673  volsup  25680  uniioombllem3  25709  mbfi1fseqlem3  25841  mbfi1fseqlem4  25842  elqaalem2  26446  aalioulem1  26458  aalioulem4  26461  aalioulem5  26462  aalioulem6  26463  aaliou  26464  aaliou3lem1  26468  aaliou3lem2  26469  aaliou3lem3  26470  aaliou3lem8  26471  aaliou3lem5  26473  aaliou3lem6  26474  aaliou3lem7  26475  taylthlem2  26499  cxpeq  26884  zrtelqelz  26885  amgmlem  27116  lgamgulmlem4  27158  lgamcvg2  27181  wilthlem2  27195  wilth  27197  wilthimp  27198  ftalem5  27203  basellem2  27208  basellem3  27209  basellem4  27210  basellem5  27211  muval1  27259  dvdssqf  27264  sgmnncl  27273  efchtdvds  27285  mumullem2  27306  mumul  27307  sqff1o  27308  fsumdvdsdiaglem  27309  dvdsppwf1o  27312  dvdsflf1o  27313  muinv  27319  mpodvdsmulf1o  27320  dvdsmulf1o  27322  chtublem  27337  fsumvma2  27340  vmasum  27342  chpchtsum  27345  logfacubnd  27347  mersenne  27353  perfect1  27354  perfectlem1  27355  perfectlem2  27356  perfect  27357  dchrelbas4  27369  dchrfi  27381  bcmono  27403  bcp1ctr  27405  bclbnd  27406  bposlem1  27410  bposlem3  27412  bposlem5  27414  bposlem6  27415  bposlem9  27418  lgsmod  27449  lgsdir  27458  lgsdilem2  27459  lgsne0  27461  lgsqrlem2  27473  lgsqr  27477  lgsqrmodndvds  27479  gausslemma2dlem0c  27484  gausslemma2dlem0h  27489  gausslemma2dlem0i  27490  gausslemma2dlem2  27493  gausslemma2dlem6  27498  gausslemma2dlem7  27499  gausslemma2d  27500  lgseisenlem1  27501  lgseisenlem2  27502  lgseisenlem3  27503  lgseisenlem4  27504  lgsquadlem1  27506  lgsquadlem2  27507  lgsquadlem3  27508  lgsquad2lem1  27510  lgsquad2lem2  27511  lgsquad2  27512  m1lgs  27514  2lgslem2  27521  2sqlem3  27546  2sqlem4  27547  2sqlem8  27552  chebbnd1lem1  27595  rplogsumlem2  27611  rpvmasumlem  27613  dchrisumlem1  27615  dchrisumlem2  27616  dchrisumlem3  27617  dchrisum0fmul  27632  dchrisum0ff  27633  dchrisum0flblem1  27634  dchrisum0flblem2  27635  dchrisum0flb  27636  dchrisum0  27646  pntrsumbnd2  27693  pntrlog2bndlem1  27703  pntrlog2bndlem6  27709  pntpbnd2  27713  pntlemg  27724  pntlemj  27729  pntlemf  27731  ostth2lem2  27760  ostth2lem3  27761  ostth3  27764  numclwlk2lem2f1o  30667  nrt2irr  30761  minvecolem4  31169  iundisj2f  32872  ssnnssfz  33069  iundisj2fi  33079  f1ocnt  33082  elq2  33093  numdenneg  33096  expgt0b  33098  ltesubnnd  33104  oexpled  33117  psgnfzto1stlem  33357  isarchi3  33444  archiabllem1b  33449  zringfrac  33785  fldextrspundgdvds  34012  cos9thpiminplylem2  34114  smatrcl  34127  1smat1  34135  submateqlem1  34138  lmatfvlem  34146  qqhval2  34313  qqhf  34317  qqhghm  34319  qqhrhm  34320  qqhnm  34321  qqhre  34351  esumcvg  34417  meascnbl  34550  omssubadd  34631  oddpwdc  34685  ballotlemfp1  34823  ballotlemfc0  34824  ballotlemfcc  34825  ballotlemimin  34837  ballotlemic  34838  ballotlem1c  34839  hgt750lemc  34975  hgt750lemd  34976  hgt750lemb  34984  hgt750leme  34986  subfaclim  35575  cvmliftlem7  35678  sinccvglem  36059  bcprod  36125  bccolsum  36126  faclimlem2  36131  faclim2  36135  poimirlem1  38155  poimirlem2  38156  poimirlem3  38157  poimirlem4  38158  poimirlem6  38160  poimirlem8  38162  poimirlem9  38163  poimirlem10  38164  poimirlem11  38165  poimirlem13  38167  poimirlem14  38168  poimirlem15  38169  poimirlem16  38170  poimirlem17  38171  poimirlem18  38172  poimirlem19  38173  poimirlem20  38174  poimirlem21  38175  poimirlem22  38176  poimirlem23  38177  poimirlem24  38178  poimirlem26  38180  poimirlem27  38181  poimirlem28  38182  poimirlem31  38185  mblfinlem2  38192  seqpo  38281  incsequz  38282  incsequz2  38283  zndvdchrrhm  42625  bccl2d  42643  nnproddivdvdsd  42652  lcmineqlem1  42681  lcmineqlem3  42683  lcmineqlem4  42684  lcmineqlem6  42686  lcmineqlem8  42688  lcmineqlem9  42689  lcmineqlem10  42690  lcmineqlem11  42691  lcmineqlem13  42693  lcmineqlem14  42694  lcmineqlem18  42698  lcmineqlem19  42699  lcmineqlem20  42700  lcmineqlem21  42701  lcmineqlem22  42702  lcmineqlem23  42703  lcmineqlem  42704  3lexlogpow5ineq2  42707  3lexlogpow2ineq1  42710  aks4d1p3  42730  aks4d1p5  42732  aks4d1p6  42733  aks4d1p8d1  42736  aks4d1p8d2  42737  aks4d1p8d3  42738  aks4d1p8  42739  aks4d1p9  42740  posbezout  42752  primrootscoprbij  42754  remexz  42756  primrootspoweq0  42758  aks6d1c1  42768  aks6d1c2p2  42771  hashscontpow1  42773  hashscontpow  42774  aks6d1c3  42775  aks6d1c4  42776  aks6d1c2lem4  42779  aks6d1c2  42782  aks6d1c5lem1  42788  sticksstones6  42803  sticksstones10  42807  sticksstones12a  42809  sticksstones12  42810  aks6d1c6lem3  42824  aks6d1c6lem4  42825  aks6d1c6isolem3  42828  aks6d1c6lem5  42829  aks6d1c7lem2  42833  aks6d1c7  42836  aks5lem1  42838  aks5lem2  42839  aks5lem3a  42841  grpods  42846  unitscyglem1  42847  unitscyglem2  42848  unitscyglem4  42850  unitscyglem5  42851  aks5  42856  sumcubes  42959  oexpreposd  42968  explt1d  42969  expeq1d  42970  expeqidd  42971  exp11d  42972  gcdle1d  42976  gcdle2d  42977  dvdsexpnn0  42980  fimgmcyc  43189  fltdvdsabdvdsc  43257  fltaccoprm  43259  fltbccoprm  43260  fltabcoprm  43261  fltne  43263  flt4lem2  43266  flt4lem3  43267  flt4lem4  43268  flt4lem5  43269  flt4lem5elem  43270  flt4lem5a  43271  flt4lem5b  43272  flt4lem5c  43273  flt4lem5d  43274  flt4lem5e  43275  flt4lem5f  43276  flt4lem6  43277  flt4lem7  43278  nna4b4nsq  43279  fltltc  43280  fltnlta  43282  irrapxlem3  43438  irrapxlem5  43440  pellexlem5  43447  pellexlem6  43448  pellex  43449  pell1234qrmulcl  43469  jm2.23  43610  jm2.20nn  43611  jm2.26lem3  43615  jm2.27a  43619  jm2.27b  43620  jm2.27c  43621  jm3.1lem1  43631  jm3.1lem3  43633  inductionexd  44768  nznngen  44913  hashnzfz2  44918  fmuldfeq  46186  divcnvg  46230  stoweidlem1  46602  stoweidlem3  46604  stoweidlem11  46612  stoweidlem20  46621  stoweidlem26  46627  stoweidlem34  46635  stoweidlem51  46652  stirlinglem4  46678  stirlinglem5  46679  stirlinglem8  46682  dirkerper  46697  dirkertrigeqlem2  46700  dirkertrigeqlem3  46701  dirkercncflem2  46705  fourierdlem11  46719  fourierdlem14  46722  fourierdlem20  46728  fourierdlem25  46733  fourierdlem37  46745  fourierdlem41  46749  fourierdlem48  46755  fourierdlem49  46756  fourierdlem54  46761  fourierdlem64  46771  fourierdlem73  46780  fourierdlem79  46786  fourierdlem92  46799  fourierdlem93  46800  fourierdlem111  46818  sqwvfourb  46830  etransclem3  46838  etransclem7  46842  etransclem10  46845  etransclem15  46850  etransclem24  46859  etransclem25  46860  etransclem26  46861  etransclem27  46862  etransclem28  46863  etransclem35  46870  etransclem37  46872  etransclem38  46873  etransclem41  46876  etransclem44  46879  etransclem45  46880  etransclem48  46883  ovnsubaddlem1  47171  vonioolem1  47281  facnn0dvdsfac  48006  muldvdsfacgt  48007  muldvdsfacm1  48008  iccpartgtprec  48053  iccpartipre  48054  fmtnoodd  48169  goldbachthlem2  48182  goldbachth  48183  odz2prm2pw  48199  fmtnoprmfac1lem  48200  fmtnoprmfac2lem1  48202  fmtnoprmfac2  48203  fmtnofac2lem  48204  2pwp1prm  48225  lighneallem1  48241  lighneallem4  48246  proththdlem  48249  proththd  48250  nprmdvdsfacm1lem4  48259  ppivalnnprm  48261  ppivalnnnprmge6  48262  divgcdoddALTV  48331  perfectALTVlem1  48370  perfectALTVlem2  48371  perfectALTV  48372  gbowge7  48412  gpgedgvtx1  48711  gpg3kgrtriexlem2  48733  gpg3kgrtriexlem5  48736  pw2m1lepw2m1  49180  nnolog2flm1  49250  dignn0fr  49261  dignn0flhalflem1  49275