Theorem nnzd 12505

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℕcn 12136  ℤcz 12479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7677  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-addrcl 11078  ax-mulcl 11079  ax-mulrcl 11080  ax-i2m1 11085  ax-1ne0 11086  ax-rnegex 11088  ax-rrecex 11089  ax-cnre 11090

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7358  df-om 7806  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-neg 11358  df-nn 12137  df-n0 12393  df-z 12480

This theorem is referenced by:  expaddzlem  14019  expmulz  14022  expmulnbnd  14149  facndiv  14202  bcval5  14232  bcpasc  14235  hashf1  14371  isercolllem1  15579  isercolllem2  15580  o1fsum  15727  bcxmas  15749  climcndslem2  15764  climcnds  15765  mertenslem1  15798  fprodser  15863  bpolydiflem  15968  eftlub  16025  eirrlem  16120  rpnnen2lem7  16136  rpnnen2lem9  16138  rpnnen2lem11  16140  sqrt2irrlem  16164  dvdsfac  16244  dvdsmod  16247  oddpwp1fsum  16310  bitsfzolem  16352  bitsmod  16354  bitsfi  16355  bitscmp  16356  bitsinv1  16360  sadadd3  16379  sadaddlem  16384  bitsuz  16392  bitsshft  16393  gcdnncl  16425  gcd1  16446  dvdsgcdidd  16455  bezoutlem3  16459  bezoutlem4  16460  mulgcd  16466  rplpwr  16476  rprpwr  16477  sqgcd  16480  expgcd  16481  nn0expgcd  16482  dvdssq  16485  lcmneg  16521  lcmgcdlem  16524  rpdvds  16578  coprmprod  16579  coprmproddvdslem  16580  congr  16582  cncongr1  16585  cncongr2  16586  prmz  16593  prmind2  16603  divgcdodd  16628  isprm6  16632  prmexpb  16637  prmfac1  16638  rpexp  16640  prmdvdsbc  16644  prmdvdsncoprmbd  16645  numdensq  16672  numdenexp  16678  hashdvds  16693  phiprmpw  16694  crth  16696  phimullem  16697  eulerthlem1  16699  eulerthlem2  16700  prmdivdiv  16705  hashgcdlem  16706  odzdvds  16714  pythagtriplem4  16738  pythagtriplem6  16740  pythagtriplem7  16741  pythagtriplem11  16744  pythagtriplem13  16746  pythagtriplem19  16752  pclem  16757  pcprendvds2  16760  pcpre1  16761  pcpremul  16762  pceulem  16764  pcqmul  16772  pcdvdsb  16788  pcidlem  16791  pcdvdstr  16795  pcgcd1  16796  pc2dvds  16798  pcprmpw2  16801  pcaddlem  16807  pcadd  16808  pcmpt2  16812  pcmptdvds  16813  pcfac  16818  pcbc  16819  qexpz  16820  oddprmdvds  16822  prmpwdvds  16823  pockthlem  16824  pockthg  16825  prmreclem2  16836  prmreclem3  16837  prmreclem4  16838  prmreclem5  16839  prmreclem6  16840  4sqlem5  16861  4sqlem8  16864  4sqlem9  16865  4sqlem10  16866  4sqlem12  16875  4sqlem14  16877  4sqlem16  16879  4sqlem17  16880  vdwlem1  16900  vdwlem2  16901  vdwlem3  16902  vdwlem6  16905  vdwlem9  16908  vdwlem10  16909  vdwnnlem3  16916  prmdvdsprmop  16962  prmolelcmf  16967  prmgaplem1  16968  prmgaplem7  16976  prmgaplem8  16977  gsumwsubmcl  18753  gsumsgrpccat  18756  gsumwmhm  18761  mulgneg  19013  mulgnndir  19024  psgnunilem4  19417  odlem2  19459  mndodconglem  19461  odmod  19466  gexlem2  19502  gexcl3  19507  gexcl2  19509  sylow1lem1  19518  sylow1lem3  19520  sylow1lem5  19522  pgpfi  19525  fislw  19545  sylow3lem4  19550  gexexlem  19772  ablfacrplem  19987  ablfacrp  19988  ablfacrp2  19989  ablfac1lem  19990  ablfac1b  19992  ablfac1eu  19995  pgpfac1lem3a  19998  ablfaclem3  20009  fincygsubgd  20033  fincygsubgodd  20034  znrrg  21511  psdpw  22104  cayhamlem1  22801  caublcls  25256  ovolicc2lem4  25468  iundisj2  25497  volsup  25504  uniioombllem3  25533  mbfi1fseqlem3  25665  mbfi1fseqlem4  25666  elqaalem2  26275  aalioulem1  26287  aalioulem4  26290  aalioulem5  26291  aalioulem6  26292  aaliou  26293  aaliou3lem1  26297  aaliou3lem2  26298  aaliou3lem3  26299  aaliou3lem8  26300  aaliou3lem5  26302  aaliou3lem6  26303  aaliou3lem7  26304  taylthlem2  26329  taylthlem2OLD  26330  cxpeq  26714  zrtelqelz  26715  amgmlem  26947  lgamgulmlem4  26989  lgamcvg2  27012  wilthlem2  27026  wilth  27028  wilthimp  27029  ftalem5  27034  basellem2  27039  basellem3  27040  basellem4  27041  basellem5  27042  muval1  27090  dvdssqf  27095  sgmnncl  27104  efchtdvds  27116  mumullem2  27137  mumul  27138  sqff1o  27139  fsumdvdsdiaglem  27140  dvdsppwf1o  27143  dvdsflf1o  27144  muinv  27150  mpodvdsmulf1o  27151  dvdsmulf1o  27153  chtublem  27169  fsumvma2  27172  vmasum  27174  chpchtsum  27177  logfacubnd  27179  mersenne  27185  perfect1  27186  perfectlem1  27187  perfectlem2  27188  perfect  27189  dchrelbas4  27201  dchrfi  27213  bcmono  27235  bcp1ctr  27237  bclbnd  27238  bposlem1  27242  bposlem3  27244  bposlem5  27246  bposlem6  27247  bposlem9  27250  lgsmod  27281  lgsdir  27290  lgsdilem2  27291  lgsne0  27293  lgsqrlem2  27305  lgsqr  27309  lgsqrmodndvds  27311  gausslemma2dlem0c  27316  gausslemma2dlem0h  27321  gausslemma2dlem0i  27322  gausslemma2dlem2  27325  gausslemma2dlem6  27330  gausslemma2dlem7  27331  gausslemma2d  27332  lgseisenlem1  27333  lgseisenlem2  27334  lgseisenlem3  27335  lgseisenlem4  27336  lgsquadlem1  27338  lgsquadlem2  27339  lgsquadlem3  27340  lgsquad2lem1  27342  lgsquad2lem2  27343  lgsquad2  27344  m1lgs  27346  2lgslem2  27353  2sqlem3  27378  2sqlem4  27379  2sqlem8  27384  chebbnd1lem1  27427  rplogsumlem2  27443  rpvmasumlem  27445  dchrisumlem1  27447  dchrisumlem2  27448  dchrisumlem3  27449  dchrisum0fmul  27464  dchrisum0ff  27465  dchrisum0flblem1  27466  dchrisum0flblem2  27467  dchrisum0flb  27468  dchrisum0  27478  pntrsumbnd2  27525  pntrlog2bndlem1  27535  pntrlog2bndlem6  27541  pntpbnd2  27545  pntlemg  27556  pntlemj  27561  pntlemf  27563  ostth2lem2  27592  ostth2lem3  27593  ostth3  27596  numclwlk2lem2f1o  30380  nrt2irr  30474  minvecolem4  30881  iundisj2f  32591  ssnnssfz  32795  iundisj2fi  32805  f1ocnt  32808  elq2  32820  numdenneg  32823  expgt0b  32825  ltesubnnd  32831  oexpled  32856  psgnfzto1stlem  33110  isarchi3  33197  archiabllem1b  33202  zringfrac  33563  fldextrspundgdvds  33766  cos9thpiminplylem2  33868  smatrcl  33881  1smat1  33889  submateqlem1  33892  lmatfvlem  33900  qqhval2  34067  qqhf  34071  qqhghm  34073  qqhrhm  34074  qqhnm  34075  qqhre  34105  esumcvg  34171  meascnbl  34304  omssubadd  34385  oddpwdc  34439  ballotlemfp1  34577  ballotlemfc0  34578  ballotlemfcc  34579  ballotlemimin  34591  ballotlemic  34592  ballotlem1c  34593  hgt750lemc  34732  hgt750lemd  34733  hgt750lemb  34741  hgt750leme  34743  subfaclim  35304  cvmliftlem7  35407  sinccvglem  35788  bcprod  35854  bccolsum  35855  faclimlem2  35860  faclim2  35864  poimirlem1  37734  poimirlem2  37735  poimirlem3  37736  poimirlem4  37737  poimirlem6  37739  poimirlem8  37741  poimirlem9  37742  poimirlem10  37743  poimirlem11  37744  poimirlem13  37746  poimirlem14  37747  poimirlem15  37748  poimirlem16  37749  poimirlem17  37750  poimirlem18  37751  poimirlem19  37752  poimirlem20  37753  poimirlem21  37754  poimirlem22  37755  poimirlem23  37756  poimirlem24  37757  poimirlem26  37759  poimirlem27  37760  poimirlem28  37761  poimirlem31  37764  mblfinlem2  37771  seqpo  37860  incsequz  37861  incsequz2  37862  zndvdchrrhm  42138  bccl2d  42157  nnproddivdvdsd  42166  lcmineqlem1  42195  lcmineqlem3  42197  lcmineqlem4  42198  lcmineqlem6  42200  lcmineqlem8  42202  lcmineqlem9  42203  lcmineqlem10  42204  lcmineqlem11  42205  lcmineqlem13  42207  lcmineqlem14  42208  lcmineqlem18  42212  lcmineqlem19  42213  lcmineqlem20  42214  lcmineqlem21  42215  lcmineqlem22  42216  lcmineqlem23  42217  lcmineqlem  42218  3lexlogpow5ineq2  42221  3lexlogpow2ineq1  42224  aks4d1p3  42244  aks4d1p5  42246  aks4d1p6  42247  aks4d1p8d1  42250  aks4d1p8d2  42251  aks4d1p8d3  42252  aks4d1p8  42253  aks4d1p9  42254  posbezout  42266  primrootscoprbij  42268  remexz  42270  primrootspoweq0  42272  aks6d1c1  42282  aks6d1c2p2  42285  hashscontpow1  42287  hashscontpow  42288  aks6d1c3  42289  aks6d1c4  42290  aks6d1c2lem4  42293  aks6d1c2  42296  aks6d1c5lem1  42302  sticksstones6  42317  sticksstones10  42321  sticksstones12a  42323  sticksstones12  42324  aks6d1c6lem3  42338  aks6d1c6lem4  42339  aks6d1c6isolem3  42342  aks6d1c6lem5  42343  aks6d1c7lem2  42347  aks6d1c7  42350  aks5lem1  42352  aks5lem2  42353  aks5lem3a  42355  grpods  42360  unitscyglem1  42361  unitscyglem2  42362  unitscyglem4  42364  unitscyglem5  42365  aks5  42370  sumcubes  42483  oexpreposd  42492  explt1d  42493  expeq1d  42494  expeqidd  42495  exp11d  42496  gcdle1d  42500  gcdle2d  42501  dvdsexpnn0  42504  fimgmcyc  42704  fltdvdsabdvdsc  42796  fltaccoprm  42798  fltbccoprm  42799  fltabcoprm  42800  fltne  42802  flt4lem2  42805  flt4lem3  42806  flt4lem4  42807  flt4lem5  42808  flt4lem5elem  42809  flt4lem5a  42810  flt4lem5b  42811  flt4lem5c  42812  flt4lem5d  42813  flt4lem5e  42814  flt4lem5f  42815  flt4lem6  42816  flt4lem7  42817  nna4b4nsq  42818  fltltc  42819  fltnlta  42821  irrapxlem3  42981  irrapxlem5  42983  pellexlem5  42990  pellexlem6  42991  pellex  42992  pell1234qrmulcl  43012  jm2.23  43153  jm2.20nn  43154  jm2.26lem3  43158  jm2.27a  43162  jm2.27b  43163  jm2.27c  43164  jm3.1lem1  43174  jm3.1lem3  43176  inductionexd  44312  nznngen  44473  hashnzfz2  44478  fmuldfeq  45745  divcnvg  45789  stoweidlem1  46161  stoweidlem3  46163  stoweidlem11  46171  stoweidlem20  46180  stoweidlem26  46186  stoweidlem34  46194  stoweidlem51  46211  stirlinglem4  46237  stirlinglem5  46238  stirlinglem8  46241  dirkerper  46256  dirkertrigeqlem2  46259  dirkertrigeqlem3  46260  dirkercncflem2  46264  fourierdlem11  46278  fourierdlem14  46281  fourierdlem20  46287  fourierdlem25  46292  fourierdlem37  46304  fourierdlem41  46308  fourierdlem48  46314  fourierdlem49  46315  fourierdlem54  46320  fourierdlem64  46330  fourierdlem73  46339  fourierdlem79  46345  fourierdlem92  46358  fourierdlem93  46359  fourierdlem111  46377  sqwvfourb  46389  etransclem3  46397  etransclem7  46401  etransclem10  46404  etransclem15  46409  etransclem24  46418  etransclem25  46419  etransclem26  46420  etransclem27  46421  etransclem28  46422  etransclem35  46429  etransclem37  46431  etransclem38  46432  etransclem41  46435  etransclem44  46438  etransclem45  46439  etransclem48  46442  ovnsubaddlem1  46730  vonioolem1  46840  iccpartgtprec  47582  iccpartipre  47583  fmtnoodd  47695  goldbachthlem2  47708  goldbachth  47709  odz2prm2pw  47725  fmtnoprmfac1lem  47726  fmtnoprmfac2lem1  47728  fmtnoprmfac2  47729  fmtnofac2lem  47730  2pwp1prm  47751  lighneallem1  47767  lighneallem4  47772  proththdlem  47775  proththd  47776  divgcdoddALTV  47844  perfectALTVlem1  47883  perfectALTVlem2  47884  perfectALTV  47885  gbowge7  47925  gpgedgvtx1  48224  gpg3kgrtriexlem2  48246  gpg3kgrtriexlem5  48249  pw2m1lepw2m1  48682  nnolog2flm1  48752  dignn0fr  48763  dignn0flhalflem1  48777