Theorem nnzd 12354

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℕcn 11903  ℤcz 12249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-i2m1 10870  ax-1ne0 10871  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-neg 11138  df-nn 11904  df-n0 12164  df-z 12250

This theorem is referenced by:  expaddzlem  13754  expmulz  13757  expmulnbnd  13878  facndiv  13930  bcval5  13960  bcpasc  13963  hashf1  14099  isercolllem1  15304  isercolllem2  15305  o1fsum  15453  bcxmas  15475  climcndslem2  15490  climcnds  15491  mertenslem1  15524  fprodser  15587  bpolydiflem  15692  eftlub  15746  eirrlem  15841  rpnnen2lem7  15857  rpnnen2lem9  15859  rpnnen2lem11  15861  sqrt2irrlem  15885  dvdsfac  15963  dvdsmod  15966  oddpwp1fsum  16029  bitsfzolem  16069  bitsmod  16071  bitsfi  16072  bitscmp  16073  bitsinv1  16077  sadadd3  16096  sadaddlem  16101  bitsuz  16109  bitsshft  16110  gcdnncl  16142  gcd1  16163  dvdsgcdidd  16173  bezoutlem3  16177  bezoutlem4  16178  mulgcd  16184  gcdmultiplezOLD  16189  rplpwr  16195  rprpwr  16196  sqgcd  16198  dvdssq  16200  lcmneg  16236  lcmgcdlem  16239  rpdvds  16293  coprmprod  16294  coprmproddvdslem  16295  congr  16297  cncongr1  16300  cncongr2  16301  prmz  16308  prmind2  16318  divgcdodd  16343  isprm6  16347  prmexpb  16353  prmfac1  16354  rpexp  16355  prmdvdsncoprmbd  16359  numdensq  16386  hashdvds  16404  phiprmpw  16405  crth  16407  phimullem  16408  eulerthlem1  16410  eulerthlem2  16411  prmdivdiv  16416  hashgcdlem  16417  odzdvds  16424  pythagtriplem4  16448  pythagtriplem6  16450  pythagtriplem7  16451  pythagtriplem11  16454  pythagtriplem13  16456  pythagtriplem19  16462  pclem  16467  pcprendvds2  16470  pcpre1  16471  pcpremul  16472  pceulem  16474  pcqmul  16482  pcdvdsb  16498  pcidlem  16501  pcdvdstr  16505  pcgcd1  16506  pc2dvds  16508  pcprmpw2  16511  pcaddlem  16517  pcadd  16518  pcmpt2  16522  pcmptdvds  16523  pcfac  16528  pcbc  16529  qexpz  16530  oddprmdvds  16532  prmpwdvds  16533  pockthlem  16534  pockthg  16535  prmreclem2  16546  prmreclem3  16547  prmreclem4  16548  prmreclem5  16549  prmreclem6  16550  4sqlem5  16571  4sqlem8  16574  4sqlem9  16575  4sqlem10  16576  4sqlem12  16585  4sqlem14  16587  4sqlem16  16589  4sqlem17  16590  vdwlem1  16610  vdwlem2  16611  vdwlem3  16612  vdwlem6  16615  vdwlem9  16618  vdwlem10  16619  vdwnnlem3  16626  prmdvdsprmop  16672  prmolelcmf  16677  prmgaplem1  16678  prmgaplem7  16686  prmgaplem8  16687  gsumwsubmcl  18390  gsumsgrpccat  18393  gsumccatOLD  18394  gsumwmhm  18399  mulgneg  18637  mulgnndir  18647  psgnunilem4  19020  odlem2  19062  mndodconglem  19064  odmod  19069  gexlem2  19102  gexcl3  19107  gexcl2  19109  sylow1lem1  19118  sylow1lem3  19120  sylow1lem5  19122  pgpfi  19125  fislw  19145  sylow3lem4  19150  gexexlem  19368  ablfacrplem  19583  ablfacrp  19584  ablfacrp2  19585  ablfac1lem  19586  ablfac1b  19588  ablfac1eu  19591  pgpfac1lem3a  19594  ablfaclem3  19605  fincygsubgd  19629  fincygsubgodd  19630  znrrg  20685  cayhamlem1  21923  caublcls  24378  ovolicc2lem4  24589  iundisj2  24618  volsup  24625  uniioombllem3  24654  mbfi1fseqlem3  24787  mbfi1fseqlem4  24788  elqaalem2  25385  aalioulem1  25397  aalioulem4  25400  aalioulem5  25401  aalioulem6  25402  aaliou  25403  aaliou3lem1  25407  aaliou3lem2  25408  aaliou3lem3  25409  aaliou3lem8  25410  aaliou3lem5  25412  aaliou3lem6  25413  aaliou3lem7  25414  taylthlem2  25438  cxpeq  25815  amgmlem  26044  lgamgulmlem4  26086  lgamcvg2  26109  wilthlem2  26123  wilth  26125  wilthimp  26126  ftalem5  26131  basellem2  26136  basellem3  26137  basellem4  26138  basellem5  26139  muval1  26187  dvdssqf  26192  sgmnncl  26201  efchtdvds  26213  mumullem2  26234  mumul  26235  sqff1o  26236  fsumdvdsdiaglem  26237  dvdsppwf1o  26240  dvdsflf1o  26241  muinv  26247  dvdsmulf1o  26248  chtublem  26264  fsumvma2  26267  vmasum  26269  chpchtsum  26272  logfacubnd  26274  mersenne  26280  perfect1  26281  perfectlem1  26282  perfectlem2  26283  perfect  26284  dchrelbas4  26296  dchrfi  26308  bcmono  26330  bcp1ctr  26332  bclbnd  26333  bposlem1  26337  bposlem3  26339  bposlem5  26341  bposlem6  26342  bposlem9  26345  lgsmod  26376  lgsdir  26385  lgsdilem2  26386  lgsne0  26388  lgsqrlem2  26400  lgsqr  26404  lgsqrmodndvds  26406  gausslemma2dlem0c  26411  gausslemma2dlem0h  26416  gausslemma2dlem0i  26417  gausslemma2dlem2  26420  gausslemma2dlem6  26425  gausslemma2dlem7  26426  gausslemma2d  26427  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem3  26430  lgseisenlem4  26431  lgsquadlem1  26433  lgsquadlem2  26434  lgsquadlem3  26435  lgsquad2lem1  26437  lgsquad2lem2  26438  lgsquad2  26439  m1lgs  26441  2lgslem2  26448  2sqlem3  26473  2sqlem4  26474  2sqlem8  26479  chebbnd1lem1  26522  rplogsumlem2  26538  rpvmasumlem  26540  dchrisumlem1  26542  dchrisumlem2  26543  dchrisumlem3  26544  dchrisum0fmul  26559  dchrisum0ff  26560  dchrisum0flblem1  26561  dchrisum0flblem2  26562  dchrisum0flb  26563  dchrisum0  26573  pntrsumbnd2  26620  pntrlog2bndlem1  26630  pntrlog2bndlem6  26636  pntpbnd2  26640  pntlemg  26651  pntlemj  26656  pntlemf  26658  ostth2lem2  26687  ostth2lem3  26688  ostth3  26691  numclwlk2lem2f1o  28644  minvecolem4  29143  iundisj2f  30830  ssnnssfz  31010  iundisj2fi  31020  f1ocnt  31025  prmdvdsbc  31032  numdenneg  31033  ltesubnnd  31038  psgnfzto1stlem  31269  isarchi3  31343  archiabllem1b  31348  smatrcl  31648  1smat1  31656  submateqlem1  31659  lmatfvlem  31667  qqhval2  31832  qqhf  31836  qqhghm  31838  qqhrhm  31839  qqhnm  31840  qqhre  31870  esumcvg  31954  meascnbl  32087  omssubadd  32167  oddpwdc  32221  ballotlemfp1  32358  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemimin  32372  ballotlemic  32373  ballotlem1c  32374  hgt750lemc  32527  hgt750lemd  32528  hgt750lemb  32536  hgt750leme  32538  subfaclim  33050  cvmliftlem7  33153  sinccvglem  33530  bcprod  33610  bccolsum  33611  faclimlem2  33616  faclim2  33620  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem6  35710  poimirlem8  35712  poimirlem9  35713  poimirlem10  35714  poimirlem11  35715  poimirlem13  35717  poimirlem14  35718  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem23  35727  poimirlem24  35728  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  poimirlem31  35735  mblfinlem2  35742  seqpo  35832  incsequz  35833  incsequz2  35834  bccl2d  39928  nnproddivdvdsd  39937  lcmineqlem1  39965  lcmineqlem3  39967  lcmineqlem4  39968  lcmineqlem6  39970  lcmineqlem8  39972  lcmineqlem9  39973  lcmineqlem10  39974  lcmineqlem11  39975  lcmineqlem13  39977  lcmineqlem14  39978  lcmineqlem18  39982  lcmineqlem19  39983  lcmineqlem20  39984  lcmineqlem21  39985  lcmineqlem22  39986  lcmineqlem23  39987  lcmineqlem  39988  3lexlogpow5ineq2  39991  3lexlogpow2ineq1  39994  aks4d1p3  40014  aks4d1p5  40016  aks4d1p6  40017  aks4d1p8d1  40020  aks4d1p8d2  40021  aks4d1p8d3  40022  aks4d1p8  40023  aks4d1p9  40024  sticksstones6  40035  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  metakunt1  40053  metakunt2  40054  metakunt3  40055  metakunt4  40056  metakunt5  40057  metakunt7  40059  metakunt10  40062  metakunt15  40067  metakunt16  40068  metakunt18  40070  metakunt19  40071  metakunt20  40072  metakunt21  40073  metakunt22  40074  metakunt24  40076  metakunt25  40077  metakunt26  40078  metakunt27  40079  metakunt28  40080  metakunt29  40081  metakunt30  40082  metakunt32  40084  metakunt33  40085  oexpreposd  40242  exp11d  40246  gcdle1d  40251  gcdle2d  40252  expgcd  40255  nn0expgcd  40256  numdenexp  40258  dvdsexpnn0  40262  zrtelqelz  40266  fltdvdsabdvdsc  40391  fltaccoprm  40393  fltbccoprm  40394  fltabcoprm  40395  fltne  40397  flt4lem2  40400  flt4lem3  40401  flt4lem4  40402  flt4lem5  40403  flt4lem5elem  40404  flt4lem5a  40405  flt4lem5b  40406  flt4lem5c  40407  flt4lem5d  40408  flt4lem5e  40409  flt4lem5f  40410  flt4lem6  40411  flt4lem7  40412  nna4b4nsq  40413  fltltc  40414  fltnlta  40416  irrapxlem3  40562  irrapxlem5  40564  pellexlem5  40571  pellexlem6  40572  pellex  40573  pell1234qrmulcl  40593  jm2.23  40734  jm2.20nn  40735  jm2.26lem3  40739  jm2.27a  40743  jm2.27b  40744  jm2.27c  40745  jm3.1lem1  40755  jm3.1lem3  40757  inductionexd  41654  nznngen  41823  hashnzfz2  41828  fmuldfeq  43014  divcnvg  43058  stoweidlem1  43432  stoweidlem3  43434  stoweidlem11  43442  stoweidlem20  43451  stoweidlem26  43457  stoweidlem34  43465  stoweidlem51  43482  stirlinglem4  43508  stirlinglem5  43509  stirlinglem8  43512  dirkerper  43527  dirkertrigeqlem2  43530  dirkertrigeqlem3  43531  dirkercncflem2  43535  fourierdlem11  43549  fourierdlem14  43552  fourierdlem20  43558  fourierdlem25  43563  fourierdlem37  43575  fourierdlem41  43579  fourierdlem48  43585  fourierdlem49  43586  fourierdlem54  43591  fourierdlem64  43601  fourierdlem73  43610  fourierdlem79  43616  fourierdlem92  43629  fourierdlem93  43630  fourierdlem111  43648  sqwvfourb  43660  etransclem3  43668  etransclem7  43672  etransclem10  43675  etransclem15  43680  etransclem24  43689  etransclem25  43690  etransclem26  43691  etransclem27  43692  etransclem28  43693  etransclem35  43700  etransclem37  43702  etransclem38  43703  etransclem41  43706  etransclem44  43709  etransclem45  43710  etransclem48  43713  ovnsubaddlem1  43998  vonioolem1  44108  iccpartgtprec  44760  iccpartipre  44761  fmtnoodd  44873  goldbachthlem2  44886  goldbachth  44887  odz2prm2pw  44903  fmtnoprmfac1lem  44904  fmtnoprmfac2lem1  44906  fmtnoprmfac2  44907  fmtnofac2lem  44908  2pwp1prm  44929  lighneallem1  44945  lighneallem4  44950  proththdlem  44953  proththd  44954  divgcdoddALTV  45022  perfectALTVlem1  45061  perfectALTVlem2  45062  perfectALTV  45063  gbowge7  45103  pw2m1lepw2m1  45749  nnolog2flm1  45824  dignn0fr  45835  dignn0flhalflem1  45849