Theorem nnzd 12490

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℕcn 12120  ℤcz 12463

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365  ax-un 7663  ax-1cn 11059  ax-icn 11060  ax-addcl 11061  ax-addrcl 11062  ax-mulcl 11063  ax-mulrcl 11064  ax-i2m1 11069  ax-1ne0 11070  ax-rnegex 11072  ax-rrecex 11073  ax-cnre 11074

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5506  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-we 5566  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-pred 6243  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-ov 7344  df-om 7792  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-neg 11342  df-nn 12121  df-n0 12377  df-z 12464

This theorem is referenced by:  expaddzlem  14007  expmulz  14010  expmulnbnd  14137  facndiv  14190  bcval5  14220  bcpasc  14223  hashf1  14359  isercolllem1  15567  isercolllem2  15568  o1fsum  15715  bcxmas  15737  climcndslem2  15752  climcnds  15753  mertenslem1  15786  fprodser  15851  bpolydiflem  15956  eftlub  16013  eirrlem  16108  rpnnen2lem7  16124  rpnnen2lem9  16126  rpnnen2lem11  16128  sqrt2irrlem  16152  dvdsfac  16232  dvdsmod  16235  oddpwp1fsum  16298  bitsfzolem  16340  bitsmod  16342  bitsfi  16343  bitscmp  16344  bitsinv1  16348  sadadd3  16367  sadaddlem  16372  bitsuz  16380  bitsshft  16381  gcdnncl  16413  gcd1  16434  dvdsgcdidd  16443  bezoutlem3  16447  bezoutlem4  16448  mulgcd  16454  rplpwr  16464  rprpwr  16465  sqgcd  16468  expgcd  16469  nn0expgcd  16470  dvdssq  16473  lcmneg  16509  lcmgcdlem  16512  rpdvds  16566  coprmprod  16567  coprmproddvdslem  16568  congr  16570  cncongr1  16573  cncongr2  16574  prmz  16581  prmind2  16591  divgcdodd  16616  isprm6  16620  prmexpb  16625  prmfac1  16626  rpexp  16628  prmdvdsbc  16632  prmdvdsncoprmbd  16633  numdensq  16660  numdenexp  16666  hashdvds  16681  phiprmpw  16682  crth  16684  phimullem  16685  eulerthlem1  16687  eulerthlem2  16688  prmdivdiv  16693  hashgcdlem  16694  odzdvds  16702  pythagtriplem4  16726  pythagtriplem6  16728  pythagtriplem7  16729  pythagtriplem11  16732  pythagtriplem13  16734  pythagtriplem19  16740  pclem  16745  pcprendvds2  16748  pcpre1  16749  pcpremul  16750  pceulem  16752  pcqmul  16760  pcdvdsb  16776  pcidlem  16779  pcdvdstr  16783  pcgcd1  16784  pc2dvds  16786  pcprmpw2  16789  pcaddlem  16795  pcadd  16796  pcmpt2  16800  pcmptdvds  16801  pcfac  16806  pcbc  16807  qexpz  16808  oddprmdvds  16810  prmpwdvds  16811  pockthlem  16812  pockthg  16813  prmreclem2  16824  prmreclem3  16825  prmreclem4  16826  prmreclem5  16827  prmreclem6  16828  4sqlem5  16849  4sqlem8  16852  4sqlem9  16853  4sqlem10  16854  4sqlem12  16863  4sqlem14  16865  4sqlem16  16867  4sqlem17  16868  vdwlem1  16888  vdwlem2  16889  vdwlem3  16890  vdwlem6  16893  vdwlem9  16896  vdwlem10  16897  vdwnnlem3  16904  prmdvdsprmop  16950  prmolelcmf  16955  prmgaplem1  16956  prmgaplem7  16964  prmgaplem8  16965  gsumwsubmcl  18740  gsumsgrpccat  18743  gsumwmhm  18748  mulgneg  19000  mulgnndir  19011  psgnunilem4  19404  odlem2  19446  mndodconglem  19448  odmod  19453  gexlem2  19489  gexcl3  19494  gexcl2  19496  sylow1lem1  19505  sylow1lem3  19507  sylow1lem5  19509  pgpfi  19512  fislw  19532  sylow3lem4  19537  gexexlem  19759  ablfacrplem  19974  ablfacrp  19975  ablfacrp2  19976  ablfac1lem  19977  ablfac1b  19979  ablfac1eu  19982  pgpfac1lem3a  19985  ablfaclem3  19996  fincygsubgd  20020  fincygsubgodd  20021  znrrg  21497  psdpw  22080  cayhamlem1  22776  caublcls  25231  ovolicc2lem4  25443  iundisj2  25472  volsup  25479  uniioombllem3  25508  mbfi1fseqlem3  25640  mbfi1fseqlem4  25641  elqaalem2  26250  aalioulem1  26262  aalioulem4  26265  aalioulem5  26266  aalioulem6  26267  aaliou  26268  aaliou3lem1  26272  aaliou3lem2  26273  aaliou3lem3  26274  aaliou3lem8  26275  aaliou3lem5  26277  aaliou3lem6  26278  aaliou3lem7  26279  taylthlem2  26304  taylthlem2OLD  26305  cxpeq  26689  zrtelqelz  26690  amgmlem  26922  lgamgulmlem4  26964  lgamcvg2  26987  wilthlem2  27001  wilth  27003  wilthimp  27004  ftalem5  27009  basellem2  27014  basellem3  27015  basellem4  27016  basellem5  27017  muval1  27065  dvdssqf  27070  sgmnncl  27079  efchtdvds  27091  mumullem2  27112  mumul  27113  sqff1o  27114  fsumdvdsdiaglem  27115  dvdsppwf1o  27118  dvdsflf1o  27119  muinv  27125  mpodvdsmulf1o  27126  dvdsmulf1o  27128  chtublem  27144  fsumvma2  27147  vmasum  27149  chpchtsum  27152  logfacubnd  27154  mersenne  27160  perfect1  27161  perfectlem1  27162  perfectlem2  27163  perfect  27164  dchrelbas4  27176  dchrfi  27188  bcmono  27210  bcp1ctr  27212  bclbnd  27213  bposlem1  27217  bposlem3  27219  bposlem5  27221  bposlem6  27222  bposlem9  27225  lgsmod  27256  lgsdir  27265  lgsdilem2  27266  lgsne0  27268  lgsqrlem2  27280  lgsqr  27284  lgsqrmodndvds  27286  gausslemma2dlem0c  27291  gausslemma2dlem0h  27296  gausslemma2dlem0i  27297  gausslemma2dlem2  27300  gausslemma2dlem6  27305  gausslemma2dlem7  27306  gausslemma2d  27307  lgseisenlem1  27308  lgseisenlem2  27309  lgseisenlem3  27310  lgseisenlem4  27311  lgsquadlem1  27313  lgsquadlem2  27314  lgsquadlem3  27315  lgsquad2lem1  27317  lgsquad2lem2  27318  lgsquad2  27319  m1lgs  27321  2lgslem2  27328  2sqlem3  27353  2sqlem4  27354  2sqlem8  27359  chebbnd1lem1  27402  rplogsumlem2  27418  rpvmasumlem  27420  dchrisumlem1  27422  dchrisumlem2  27423  dchrisumlem3  27424  dchrisum0fmul  27439  dchrisum0ff  27440  dchrisum0flblem1  27441  dchrisum0flblem2  27442  dchrisum0flb  27443  dchrisum0  27453  pntrsumbnd2  27500  pntrlog2bndlem1  27510  pntrlog2bndlem6  27516  pntpbnd2  27520  pntlemg  27531  pntlemj  27536  pntlemf  27538  ostth2lem2  27567  ostth2lem3  27568  ostth3  27571  numclwlk2lem2f1o  30351  nrt2irr  30445  minvecolem4  30852  iundisj2f  32562  ssnnssfz  32762  iundisj2fi  32771  f1ocnt  32774  elq2  32786  numdenneg  32789  expgt0b  32791  ltesubnnd  32797  oexpled  32822  psgnfzto1stlem  33061  isarchi3  33148  archiabllem1b  33153  zringfrac  33511  fldextrspundgdvds  33686  cos9thpiminplylem2  33788  smatrcl  33801  1smat1  33809  submateqlem1  33812  lmatfvlem  33820  qqhval2  33987  qqhf  33991  qqhghm  33993  qqhrhm  33994  qqhnm  33995  qqhre  34025  esumcvg  34091  meascnbl  34224  omssubadd  34305  oddpwdc  34359  ballotlemfp1  34497  ballotlemfc0  34498  ballotlemfcc  34499  ballotlemimin  34511  ballotlemic  34512  ballotlem1c  34513  hgt750lemc  34652  hgt750lemd  34653  hgt750lemb  34661  hgt750leme  34663  subfaclim  35224  cvmliftlem7  35327  sinccvglem  35708  bcprod  35774  bccolsum  35775  faclimlem2  35780  faclim2  35784  poimirlem1  37661  poimirlem2  37662  poimirlem3  37663  poimirlem4  37664  poimirlem6  37666  poimirlem8  37668  poimirlem9  37669  poimirlem10  37670  poimirlem11  37671  poimirlem13  37673  poimirlem14  37674  poimirlem15  37675  poimirlem16  37676  poimirlem17  37677  poimirlem18  37678  poimirlem19  37679  poimirlem20  37680  poimirlem21  37681  poimirlem22  37682  poimirlem23  37683  poimirlem24  37684  poimirlem26  37686  poimirlem27  37687  poimirlem28  37688  poimirlem31  37691  mblfinlem2  37698  seqpo  37787  incsequz  37788  incsequz2  37789  zndvdchrrhm  42005  bccl2d  42024  nnproddivdvdsd  42033  lcmineqlem1  42062  lcmineqlem3  42064  lcmineqlem4  42065  lcmineqlem6  42067  lcmineqlem8  42069  lcmineqlem9  42070  lcmineqlem10  42071  lcmineqlem11  42072  lcmineqlem13  42074  lcmineqlem14  42075  lcmineqlem18  42079  lcmineqlem19  42080  lcmineqlem20  42081  lcmineqlem21  42082  lcmineqlem22  42083  lcmineqlem23  42084  lcmineqlem  42085  3lexlogpow5ineq2  42088  3lexlogpow2ineq1  42091  aks4d1p3  42111  aks4d1p5  42113  aks4d1p6  42114  aks4d1p8d1  42117  aks4d1p8d2  42118  aks4d1p8d3  42119  aks4d1p8  42120  aks4d1p9  42121  posbezout  42133  primrootscoprbij  42135  remexz  42137  primrootspoweq0  42139  aks6d1c1  42149  aks6d1c2p2  42152  hashscontpow1  42154  hashscontpow  42155  aks6d1c3  42156  aks6d1c4  42157  aks6d1c2lem4  42160  aks6d1c2  42163  aks6d1c5lem1  42169  sticksstones6  42184  sticksstones10  42188  sticksstones12a  42190  sticksstones12  42191  aks6d1c6lem3  42205  aks6d1c6lem4  42206  aks6d1c6isolem3  42209  aks6d1c6lem5  42210  aks6d1c7lem2  42214  aks6d1c7  42217  aks5lem1  42219  aks5lem2  42220  aks5lem3a  42222  grpods  42227  unitscyglem1  42228  unitscyglem2  42229  unitscyglem4  42231  unitscyglem5  42232  aks5  42237  sumcubes  42346  oexpreposd  42355  explt1d  42356  expeq1d  42357  expeqidd  42358  exp11d  42359  gcdle1d  42363  gcdle2d  42364  dvdsexpnn0  42367  fimgmcyc  42567  fltdvdsabdvdsc  42671  fltaccoprm  42673  fltbccoprm  42674  fltabcoprm  42675  fltne  42677  flt4lem2  42680  flt4lem3  42681  flt4lem4  42682  flt4lem5  42683  flt4lem5elem  42684  flt4lem5a  42685  flt4lem5b  42686  flt4lem5c  42687  flt4lem5d  42688  flt4lem5e  42689  flt4lem5f  42690  flt4lem6  42691  flt4lem7  42692  nna4b4nsq  42693  fltltc  42694  fltnlta  42696  irrapxlem3  42857  irrapxlem5  42859  pellexlem5  42866  pellexlem6  42867  pellex  42868  pell1234qrmulcl  42888  jm2.23  43029  jm2.20nn  43030  jm2.26lem3  43034  jm2.27a  43038  jm2.27b  43039  jm2.27c  43040  jm3.1lem1  43050  jm3.1lem3  43052  inductionexd  44188  nznngen  44349  hashnzfz2  44354  fmuldfeq  45623  divcnvg  45667  stoweidlem1  46039  stoweidlem3  46041  stoweidlem11  46049  stoweidlem20  46058  stoweidlem26  46064  stoweidlem34  46072  stoweidlem51  46089  stirlinglem4  46115  stirlinglem5  46116  stirlinglem8  46119  dirkerper  46134  dirkertrigeqlem2  46137  dirkertrigeqlem3  46138  dirkercncflem2  46142  fourierdlem11  46156  fourierdlem14  46159  fourierdlem20  46165  fourierdlem25  46170  fourierdlem37  46182  fourierdlem41  46186  fourierdlem48  46192  fourierdlem49  46193  fourierdlem54  46198  fourierdlem64  46208  fourierdlem73  46217  fourierdlem79  46223  fourierdlem92  46236  fourierdlem93  46237  fourierdlem111  46255  sqwvfourb  46267  etransclem3  46275  etransclem7  46279  etransclem10  46282  etransclem15  46287  etransclem24  46296  etransclem25  46297  etransclem26  46298  etransclem27  46299  etransclem28  46300  etransclem35  46307  etransclem37  46309  etransclem38  46310  etransclem41  46313  etransclem44  46316  etransclem45  46317  etransclem48  46320  ovnsubaddlem1  46608  vonioolem1  46718  iccpartgtprec  47451  iccpartipre  47452  fmtnoodd  47564  goldbachthlem2  47577  goldbachth  47578  odz2prm2pw  47594  fmtnoprmfac1lem  47595  fmtnoprmfac2lem1  47597  fmtnoprmfac2  47598  fmtnofac2lem  47599  2pwp1prm  47620  lighneallem1  47636  lighneallem4  47641  proththdlem  47644  proththd  47645  divgcdoddALTV  47713  perfectALTVlem1  47752  perfectALTVlem2  47753  perfectALTV  47754  gbowge7  47794  gpgedgvtx1  48093  gpg3kgrtriexlem2  48115  gpg3kgrtriexlem5  48118  pw2m1lepw2m1  48552  nnolog2flm1  48622  dignn0fr  48633  dignn0flhalflem1  48647