Theorem nnzd 12424

Description: A nonnegative 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 12293	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	2	nn0zd 12423	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2110  ℕcn 11973  ℤcz 12319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356  ax-un 7582  ax-1cn 10930  ax-icn 10931  ax-addcl 10932  ax-addrcl 10933  ax-mulcl 10934  ax-mulrcl 10935  ax-i2m1 10940  ax-1ne0 10941  ax-rnegex 10943  ax-rrecex 10944  ax-cnre 10945

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6201  df-ord 6268  df-on 6269  df-lim 6270  df-suc 6271  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-ov 7274  df-om 7707  df-2nd 7825  df-frecs 8088  df-wrecs 8119  df-recs 8193  df-rdg 8232  df-neg 11208  df-nn 11974  df-n0 12234  df-z 12320

This theorem is referenced by:  expaddzlem  13824  expmulz  13827  expmulnbnd  13948  facndiv  14000  bcval5  14030  bcpasc  14033  hashf1  14169  isercolllem1  15374  isercolllem2  15375  o1fsum  15523  bcxmas  15545  climcndslem2  15560  climcnds  15561  mertenslem1  15594  fprodser  15657  bpolydiflem  15762  eftlub  15816  eirrlem  15911  rpnnen2lem7  15927  rpnnen2lem9  15929  rpnnen2lem11  15931  sqrt2irrlem  15955  dvdsfac  16033  dvdsmod  16036  oddpwp1fsum  16099  bitsfzolem  16139  bitsmod  16141  bitsfi  16142  bitscmp  16143  bitsinv1  16147  sadadd3  16166  sadaddlem  16171  bitsuz  16179  bitsshft  16180  gcdnncl  16212  gcd1  16233  dvdsgcdidd  16243  bezoutlem3  16247  bezoutlem4  16248  mulgcd  16254  gcdmultiplezOLD  16259  rplpwr  16265  rprpwr  16266  sqgcd  16268  dvdssq  16270  lcmneg  16306  lcmgcdlem  16309  rpdvds  16363  coprmprod  16364  coprmproddvdslem  16365  congr  16367  cncongr1  16370  cncongr2  16371  prmz  16378  prmind2  16388  divgcdodd  16413  isprm6  16417  prmexpb  16423  prmfac1  16424  rpexp  16425  prmdvdsncoprmbd  16429  numdensq  16456  hashdvds  16474  phiprmpw  16475  crth  16477  phimullem  16478  eulerthlem1  16480  eulerthlem2  16481  prmdivdiv  16486  hashgcdlem  16487  odzdvds  16494  pythagtriplem4  16518  pythagtriplem6  16520  pythagtriplem7  16521  pythagtriplem11  16524  pythagtriplem13  16526  pythagtriplem19  16532  pclem  16537  pcprendvds2  16540  pcpre1  16541  pcpremul  16542  pceulem  16544  pcqmul  16552  pcdvdsb  16568  pcidlem  16571  pcdvdstr  16575  pcgcd1  16576  pc2dvds  16578  pcprmpw2  16581  pcaddlem  16587  pcadd  16588  pcmpt2  16592  pcmptdvds  16593  pcfac  16598  pcbc  16599  qexpz  16600  oddprmdvds  16602  prmpwdvds  16603  pockthlem  16604  pockthg  16605  prmreclem2  16616  prmreclem3  16617  prmreclem4  16618  prmreclem5  16619  prmreclem6  16620  4sqlem5  16641  4sqlem8  16644  4sqlem9  16645  4sqlem10  16646  4sqlem12  16655  4sqlem14  16657  4sqlem16  16659  4sqlem17  16660  vdwlem1  16680  vdwlem2  16681  vdwlem3  16682  vdwlem6  16685  vdwlem9  16688  vdwlem10  16689  vdwnnlem3  16696  prmdvdsprmop  16742  prmolelcmf  16747  prmgaplem1  16748  prmgaplem7  16756  prmgaplem8  16757  gsumwsubmcl  18473  gsumsgrpccat  18476  gsumccatOLD  18477  gsumwmhm  18482  mulgneg  18720  mulgnndir  18730  psgnunilem4  19103  odlem2  19145  mndodconglem  19147  odmod  19152  gexlem2  19185  gexcl3  19190  gexcl2  19192  sylow1lem1  19201  sylow1lem3  19203  sylow1lem5  19205  pgpfi  19208  fislw  19228  sylow3lem4  19233  gexexlem  19451  ablfacrplem  19666  ablfacrp  19667  ablfacrp2  19668  ablfac1lem  19669  ablfac1b  19671  ablfac1eu  19674  pgpfac1lem3a  19677  ablfaclem3  19688  fincygsubgd  19712  fincygsubgodd  19713  znrrg  20771  cayhamlem1  22013  caublcls  24471  ovolicc2lem4  24682  iundisj2  24711  volsup  24718  uniioombllem3  24747  mbfi1fseqlem3  24880  mbfi1fseqlem4  24881  elqaalem2  25478  aalioulem1  25490  aalioulem4  25493  aalioulem5  25494  aalioulem6  25495  aaliou  25496  aaliou3lem1  25500  aaliou3lem2  25501  aaliou3lem3  25502  aaliou3lem8  25503  aaliou3lem5  25505  aaliou3lem6  25506  aaliou3lem7  25507  taylthlem2  25531  cxpeq  25908  amgmlem  26137  lgamgulmlem4  26179  lgamcvg2  26202  wilthlem2  26216  wilth  26218  wilthimp  26219  ftalem5  26224  basellem2  26229  basellem3  26230  basellem4  26231  basellem5  26232  muval1  26280  dvdssqf  26285  sgmnncl  26294  efchtdvds  26306  mumullem2  26327  mumul  26328  sqff1o  26329  fsumdvdsdiaglem  26330  dvdsppwf1o  26333  dvdsflf1o  26334  muinv  26340  dvdsmulf1o  26341  chtublem  26357  fsumvma2  26360  vmasum  26362  chpchtsum  26365  logfacubnd  26367  mersenne  26373  perfect1  26374  perfectlem1  26375  perfectlem2  26376  perfect  26377  dchrelbas4  26389  dchrfi  26401  bcmono  26423  bcp1ctr  26425  bclbnd  26426  bposlem1  26430  bposlem3  26432  bposlem5  26434  bposlem6  26435  bposlem9  26438  lgsmod  26469  lgsdir  26478  lgsdilem2  26479  lgsne0  26481  lgsqrlem2  26493  lgsqr  26497  lgsqrmodndvds  26499  gausslemma2dlem0c  26504  gausslemma2dlem0h  26509  gausslemma2dlem0i  26510  gausslemma2dlem2  26513  gausslemma2dlem6  26518  gausslemma2dlem7  26519  gausslemma2d  26520  lgseisenlem1  26521  lgseisenlem2  26522  lgseisenlem3  26523  lgseisenlem4  26524  lgsquadlem1  26526  lgsquadlem2  26527  lgsquadlem3  26528  lgsquad2lem1  26530  lgsquad2lem2  26531  lgsquad2  26532  m1lgs  26534  2lgslem2  26541  2sqlem3  26566  2sqlem4  26567  2sqlem8  26572  chebbnd1lem1  26615  rplogsumlem2  26631  rpvmasumlem  26633  dchrisumlem1  26635  dchrisumlem2  26636  dchrisumlem3  26637  dchrisum0fmul  26652  dchrisum0ff  26653  dchrisum0flblem1  26654  dchrisum0flblem2  26655  dchrisum0flb  26656  dchrisum0  26666  pntrsumbnd2  26713  pntrlog2bndlem1  26723  pntrlog2bndlem6  26729  pntpbnd2  26733  pntlemg  26744  pntlemj  26749  pntlemf  26751  ostth2lem2  26780  ostth2lem3  26781  ostth3  26784  numclwlk2lem2f1o  28739  minvecolem4  29238  iundisj2f  30925  ssnnssfz  31104  iundisj2fi  31114  f1ocnt  31119  prmdvdsbc  31126  numdenneg  31127  ltesubnnd  31132  psgnfzto1stlem  31363  isarchi3  31437  archiabllem1b  31442  smatrcl  31742  1smat1  31750  submateqlem1  31753  lmatfvlem  31761  qqhval2  31928  qqhf  31932  qqhghm  31934  qqhrhm  31935  qqhnm  31936  qqhre  31966  esumcvg  32050  meascnbl  32183  omssubadd  32263  oddpwdc  32317  ballotlemfp1  32454  ballotlemfc0  32455  ballotlemfcc  32456  ballotlemimin  32468  ballotlemic  32469  ballotlem1c  32470  hgt750lemc  32623  hgt750lemd  32624  hgt750lemb  32632  hgt750leme  32634  subfaclim  33146  cvmliftlem7  33249  sinccvglem  33626  bcprod  33700  bccolsum  33701  faclimlem2  33706  faclim2  33710  poimirlem1  35774  poimirlem2  35775  poimirlem3  35776  poimirlem4  35777  poimirlem6  35779  poimirlem8  35781  poimirlem9  35782  poimirlem10  35783  poimirlem11  35784  poimirlem13  35786  poimirlem14  35787  poimirlem15  35788  poimirlem16  35789  poimirlem17  35790  poimirlem18  35791  poimirlem19  35792  poimirlem20  35793  poimirlem21  35794  poimirlem22  35795  poimirlem23  35796  poimirlem24  35797  poimirlem26  35799  poimirlem27  35800  poimirlem28  35801  poimirlem31  35804  mblfinlem2  35811  seqpo  35901  incsequz  35902  incsequz2  35903  bccl2d  39997  nnproddivdvdsd  40006  lcmineqlem1  40034  lcmineqlem3  40036  lcmineqlem4  40037  lcmineqlem6  40039  lcmineqlem8  40041  lcmineqlem9  40042  lcmineqlem10  40043  lcmineqlem11  40044  lcmineqlem13  40046  lcmineqlem14  40047  lcmineqlem18  40051  lcmineqlem19  40052  lcmineqlem20  40053  lcmineqlem21  40054  lcmineqlem22  40055  lcmineqlem23  40056  lcmineqlem  40057  3lexlogpow5ineq2  40060  3lexlogpow2ineq1  40063  aks4d1p3  40083  aks4d1p5  40085  aks4d1p6  40086  aks4d1p8d1  40089  aks4d1p8d2  40090  aks4d1p8d3  40091  aks4d1p8  40092  aks4d1p9  40093  sticksstones6  40104  sticksstones10  40108  sticksstones12a  40110  sticksstones12  40111  metakunt1  40122  metakunt2  40123  metakunt3  40124  metakunt4  40125  metakunt5  40126  metakunt7  40128  metakunt10  40131  metakunt15  40136  metakunt16  40137  metakunt18  40139  metakunt19  40140  metakunt20  40141  metakunt21  40142  metakunt22  40143  metakunt24  40145  metakunt25  40146  metakunt26  40147  metakunt27  40148  metakunt28  40149  metakunt29  40150  metakunt30  40151  metakunt32  40153  metakunt33  40154  oexpreposd  40318  exp11d  40322  gcdle1d  40327  gcdle2d  40328  expgcd  40331  nn0expgcd  40332  numdenexp  40334  dvdsexpnn0  40338  zrtelqelz  40342  fltdvdsabdvdsc  40472  fltaccoprm  40474  fltbccoprm  40475  fltabcoprm  40476  fltne  40478  flt4lem2  40481  flt4lem3  40482  flt4lem4  40483  flt4lem5  40484  flt4lem5elem  40485  flt4lem5a  40486  flt4lem5b  40487  flt4lem5c  40488  flt4lem5d  40489  flt4lem5e  40490  flt4lem5f  40491  flt4lem6  40492  flt4lem7  40493  nna4b4nsq  40494  fltltc  40495  fltnlta  40497  irrapxlem3  40643  irrapxlem5  40645  pellexlem5  40652  pellexlem6  40653  pellex  40654  pell1234qrmulcl  40674  jm2.23  40815  jm2.20nn  40816  jm2.26lem3  40820  jm2.27a  40824  jm2.27b  40825  jm2.27c  40826  jm3.1lem1  40836  jm3.1lem3  40838  inductionexd  41735  nznngen  41904  hashnzfz2  41909  fmuldfeq  43095  divcnvg  43139  stoweidlem1  43513  stoweidlem3  43515  stoweidlem11  43523  stoweidlem20  43532  stoweidlem26  43538  stoweidlem34  43546  stoweidlem51  43563  stirlinglem4  43589  stirlinglem5  43590  stirlinglem8  43593  dirkerper  43608  dirkertrigeqlem2  43611  dirkertrigeqlem3  43612  dirkercncflem2  43616  fourierdlem11  43630  fourierdlem14  43633  fourierdlem20  43639  fourierdlem25  43644  fourierdlem37  43656  fourierdlem41  43660  fourierdlem48  43666  fourierdlem49  43667  fourierdlem54  43672  fourierdlem64  43682  fourierdlem73  43691  fourierdlem79  43697  fourierdlem92  43710  fourierdlem93  43711  fourierdlem111  43729  sqwvfourb  43741  etransclem3  43749  etransclem7  43753  etransclem10  43756  etransclem15  43761  etransclem24  43770  etransclem25  43771  etransclem26  43772  etransclem27  43773  etransclem28  43774  etransclem35  43781  etransclem37  43783  etransclem38  43784  etransclem41  43787  etransclem44  43790  etransclem45  43791  etransclem48  43794  ovnsubaddlem1  44079  vonioolem1  44189  iccpartgtprec  44841  iccpartipre  44842  fmtnoodd  44954  goldbachthlem2  44967  goldbachth  44968  odz2prm2pw  44984  fmtnoprmfac1lem  44985  fmtnoprmfac2lem1  44987  fmtnoprmfac2  44988  fmtnofac2lem  44989  2pwp1prm  45010  lighneallem1  45026  lighneallem4  45031  proththdlem  45034  proththd  45035  divgcdoddALTV  45103  perfectALTVlem1  45142  perfectALTVlem2  45143  perfectALTV  45144  gbowge7  45184  pw2m1lepw2m1  45830  nnolog2flm1  45905  dignn0fr  45916  dignn0flhalflem1  45930