Theorem nnzd 12281

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

Syntax hints:   → wi 4   ∈ wcel 2110  ℕcn 11830  ℤcz 12176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322  ax-un 7523  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-i2m1 10797  ax-1ne0 10798  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-ov 7216  df-om 7645  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-neg 11065  df-nn 11831  df-n0 12091  df-z 12177

This theorem is referenced by:  expaddzlem  13678  expmulz  13681  expmulnbnd  13802  facndiv  13854  bcval5  13884  bcpasc  13887  hashf1  14023  isercolllem1  15228  isercolllem2  15229  o1fsum  15377  bcxmas  15399  climcndslem2  15414  climcnds  15415  mertenslem1  15448  fprodser  15511  bpolydiflem  15616  eftlub  15670  eirrlem  15765  rpnnen2lem7  15781  rpnnen2lem9  15783  rpnnen2lem11  15785  sqrt2irrlem  15809  dvdsfac  15887  dvdsmod  15890  oddpwp1fsum  15953  bitsfzolem  15993  bitsmod  15995  bitsfi  15996  bitscmp  15997  bitsinv1  16001  sadadd3  16020  sadaddlem  16025  bitsuz  16033  bitsshft  16034  gcdnncl  16066  gcd1  16087  dvdsgcdidd  16097  bezoutlem3  16101  bezoutlem4  16102  mulgcd  16108  gcdmultiplezOLD  16113  rplpwr  16119  rprpwr  16120  sqgcd  16122  dvdssq  16124  lcmneg  16160  lcmgcdlem  16163  rpdvds  16217  coprmprod  16218  coprmproddvdslem  16219  congr  16221  cncongr1  16224  cncongr2  16225  prmz  16232  prmind2  16242  divgcdodd  16267  isprm6  16271  prmexpb  16277  prmfac1  16278  rpexp  16279  prmdvdsncoprmbd  16283  numdensq  16310  hashdvds  16328  phiprmpw  16329  crth  16331  phimullem  16332  eulerthlem1  16334  eulerthlem2  16335  prmdivdiv  16340  hashgcdlem  16341  odzdvds  16348  pythagtriplem4  16372  pythagtriplem6  16374  pythagtriplem7  16375  pythagtriplem11  16378  pythagtriplem13  16380  pythagtriplem19  16386  pclem  16391  pcprendvds2  16394  pcpre1  16395  pcpremul  16396  pceulem  16398  pcqmul  16406  pcdvdsb  16422  pcidlem  16425  pcdvdstr  16429  pcgcd1  16430  pc2dvds  16432  pcprmpw2  16435  pcaddlem  16441  pcadd  16442  pcmpt2  16446  pcmptdvds  16447  pcfac  16452  pcbc  16453  qexpz  16454  oddprmdvds  16456  prmpwdvds  16457  pockthlem  16458  pockthg  16459  prmreclem2  16470  prmreclem3  16471  prmreclem4  16472  prmreclem5  16473  prmreclem6  16474  4sqlem5  16495  4sqlem8  16498  4sqlem9  16499  4sqlem10  16500  4sqlem12  16509  4sqlem14  16511  4sqlem16  16513  4sqlem17  16514  vdwlem1  16534  vdwlem2  16535  vdwlem3  16536  vdwlem6  16539  vdwlem9  16542  vdwlem10  16543  vdwnnlem3  16550  prmdvdsprmop  16596  prmolelcmf  16601  prmgaplem1  16602  prmgaplem7  16610  prmgaplem8  16611  gsumwsubmcl  18263  gsumsgrpccat  18266  gsumccatOLD  18267  gsumwmhm  18272  mulgneg  18510  mulgnndir  18520  psgnunilem4  18889  odlem2  18931  mndodconglem  18933  odmod  18938  gexlem2  18971  gexcl3  18976  gexcl2  18978  sylow1lem1  18987  sylow1lem3  18989  sylow1lem5  18991  pgpfi  18994  fislw  19014  sylow3lem4  19019  gexexlem  19237  ablfacrplem  19452  ablfacrp  19453  ablfacrp2  19454  ablfac1lem  19455  ablfac1b  19457  ablfac1eu  19460  pgpfac1lem3a  19463  ablfaclem3  19474  fincygsubgd  19498  fincygsubgodd  19499  znrrg  20530  cayhamlem1  21763  caublcls  24206  ovolicc2lem4  24417  iundisj2  24446  volsup  24453  uniioombllem3  24482  mbfi1fseqlem3  24615  mbfi1fseqlem4  24616  elqaalem2  25213  aalioulem1  25225  aalioulem4  25228  aalioulem5  25229  aalioulem6  25230  aaliou  25231  aaliou3lem1  25235  aaliou3lem2  25236  aaliou3lem3  25237  aaliou3lem8  25238  aaliou3lem5  25240  aaliou3lem6  25241  aaliou3lem7  25242  taylthlem2  25266  cxpeq  25643  amgmlem  25872  lgamgulmlem4  25914  lgamcvg2  25937  wilthlem2  25951  wilth  25953  wilthimp  25954  ftalem5  25959  basellem2  25964  basellem3  25965  basellem4  25966  basellem5  25967  muval1  26015  dvdssqf  26020  sgmnncl  26029  efchtdvds  26041  mumullem2  26062  mumul  26063  sqff1o  26064  fsumdvdsdiaglem  26065  dvdsppwf1o  26068  dvdsflf1o  26069  muinv  26075  dvdsmulf1o  26076  chtublem  26092  fsumvma2  26095  vmasum  26097  chpchtsum  26100  logfacubnd  26102  mersenne  26108  perfect1  26109  perfectlem1  26110  perfectlem2  26111  perfect  26112  dchrelbas4  26124  dchrfi  26136  bcmono  26158  bcp1ctr  26160  bclbnd  26161  bposlem1  26165  bposlem3  26167  bposlem5  26169  bposlem6  26170  bposlem9  26173  lgsmod  26204  lgsdir  26213  lgsdilem2  26214  lgsne0  26216  lgsqrlem2  26228  lgsqr  26232  lgsqrmodndvds  26234  gausslemma2dlem0c  26239  gausslemma2dlem0h  26244  gausslemma2dlem0i  26245  gausslemma2dlem2  26248  gausslemma2dlem6  26253  gausslemma2dlem7  26254  gausslemma2d  26255  lgseisenlem1  26256  lgseisenlem2  26257  lgseisenlem3  26258  lgseisenlem4  26259  lgsquadlem1  26261  lgsquadlem2  26262  lgsquadlem3  26263  lgsquad2lem1  26265  lgsquad2lem2  26266  lgsquad2  26267  m1lgs  26269  2lgslem2  26276  2sqlem3  26301  2sqlem4  26302  2sqlem8  26307  chebbnd1lem1  26350  rplogsumlem2  26366  rpvmasumlem  26368  dchrisumlem1  26370  dchrisumlem2  26371  dchrisumlem3  26372  dchrisum0fmul  26387  dchrisum0ff  26388  dchrisum0flblem1  26389  dchrisum0flblem2  26390  dchrisum0flb  26391  dchrisum0  26401  pntrsumbnd2  26448  pntrlog2bndlem1  26458  pntrlog2bndlem6  26464  pntpbnd2  26468  pntlemg  26479  pntlemj  26484  pntlemf  26486  ostth2lem2  26515  ostth2lem3  26516  ostth3  26519  numclwlk2lem2f1o  28462  minvecolem4  28961  iundisj2f  30648  ssnnssfz  30828  iundisj2fi  30838  f1ocnt  30843  prmdvdsbc  30850  numdenneg  30851  ltesubnnd  30856  psgnfzto1stlem  31086  isarchi3  31160  archiabllem1b  31165  smatrcl  31460  1smat1  31468  submateqlem1  31471  lmatfvlem  31479  qqhval2  31644  qqhf  31648  qqhghm  31650  qqhrhm  31651  qqhnm  31652  qqhre  31682  esumcvg  31766  meascnbl  31899  omssubadd  31979  oddpwdc  32033  ballotlemfp1  32170  ballotlemfc0  32171  ballotlemfcc  32172  ballotlemimin  32184  ballotlemic  32185  ballotlem1c  32186  hgt750lemc  32339  hgt750lemd  32340  hgt750lemb  32348  hgt750leme  32350  subfaclim  32863  cvmliftlem7  32966  sinccvglem  33343  bcprod  33422  bccolsum  33423  faclimlem2  33428  faclim2  33432  poimirlem1  35515  poimirlem2  35516  poimirlem3  35517  poimirlem4  35518  poimirlem6  35520  poimirlem8  35522  poimirlem9  35523  poimirlem10  35524  poimirlem11  35525  poimirlem13  35527  poimirlem14  35528  poimirlem15  35529  poimirlem16  35530  poimirlem17  35531  poimirlem18  35532  poimirlem19  35533  poimirlem20  35534  poimirlem21  35535  poimirlem22  35536  poimirlem23  35537  poimirlem24  35538  poimirlem26  35540  poimirlem27  35541  poimirlem28  35542  poimirlem31  35545  mblfinlem2  35552  seqpo  35642  incsequz  35643  incsequz2  35644  bccl2d  39734  nnproddivdvdsd  39743  lcmineqlem1  39771  lcmineqlem3  39773  lcmineqlem4  39774  lcmineqlem6  39776  lcmineqlem8  39778  lcmineqlem9  39779  lcmineqlem10  39780  lcmineqlem11  39781  lcmineqlem13  39783  lcmineqlem14  39784  lcmineqlem18  39788  lcmineqlem19  39789  lcmineqlem20  39790  lcmineqlem21  39791  lcmineqlem22  39792  lcmineqlem23  39793  lcmineqlem  39794  3lexlogpow5ineq2  39797  3lexlogpow2ineq1  39800  aks4d1p3  39819  sticksstones6  39829  sticksstones10  39833  sticksstones12a  39835  sticksstones12  39836  metakunt1  39847  metakunt2  39848  metakunt3  39849  metakunt4  39850  metakunt5  39851  metakunt7  39853  metakunt10  39856  metakunt15  39861  metakunt16  39862  metakunt18  39864  metakunt19  39865  metakunt20  39866  metakunt21  39867  metakunt22  39868  metakunt24  39870  metakunt25  39871  metakunt26  39872  metakunt27  39873  metakunt28  39874  metakunt29  39875  metakunt30  39876  metakunt32  39878  metakunt33  39879  oexpreposd  40028  exp11d  40033  gcdle1d  40038  gcdle2d  40039  expgcd  40042  nn0expgcd  40043  numdenexp  40045  dvdsexpnn0  40049  zrtelqelz  40053  fltdvdsabdvdsc  40178  fltaccoprm  40180  fltbccoprm  40181  fltabcoprm  40182  fltne  40184  flt4lem2  40187  flt4lem3  40188  flt4lem4  40189  flt4lem5  40190  flt4lem5elem  40191  flt4lem5a  40192  flt4lem5b  40193  flt4lem5c  40194  flt4lem5d  40195  flt4lem5e  40196  flt4lem5f  40197  flt4lem6  40198  flt4lem7  40199  nna4b4nsq  40200  fltltc  40201  fltnlta  40203  irrapxlem3  40349  irrapxlem5  40351  pellexlem5  40358  pellexlem6  40359  pellex  40360  pell1234qrmulcl  40380  jm2.23  40521  jm2.20nn  40522  jm2.26lem3  40526  jm2.27a  40530  jm2.27b  40531  jm2.27c  40532  jm3.1lem1  40542  jm3.1lem3  40544  inductionexd  41442  nznngen  41607  hashnzfz2  41612  fmuldfeq  42799  divcnvg  42843  stoweidlem1  43217  stoweidlem3  43219  stoweidlem11  43227  stoweidlem20  43236  stoweidlem26  43242  stoweidlem34  43250  stoweidlem51  43267  stirlinglem4  43293  stirlinglem5  43294  stirlinglem8  43297  dirkerper  43312  dirkertrigeqlem2  43315  dirkertrigeqlem3  43316  dirkercncflem2  43320  fourierdlem11  43334  fourierdlem14  43337  fourierdlem20  43343  fourierdlem25  43348  fourierdlem37  43360  fourierdlem41  43364  fourierdlem48  43370  fourierdlem49  43371  fourierdlem54  43376  fourierdlem64  43386  fourierdlem73  43395  fourierdlem79  43401  fourierdlem92  43414  fourierdlem93  43415  fourierdlem111  43433  sqwvfourb  43445  etransclem3  43453  etransclem7  43457  etransclem10  43460  etransclem15  43465  etransclem24  43474  etransclem25  43475  etransclem26  43476  etransclem27  43477  etransclem28  43478  etransclem35  43485  etransclem37  43487  etransclem38  43488  etransclem41  43491  etransclem44  43494  etransclem45  43495  etransclem48  43498  ovnsubaddlem1  43783  vonioolem1  43893  iccpartgtprec  44545  iccpartipre  44546  fmtnoodd  44658  goldbachthlem2  44671  goldbachth  44672  odz2prm2pw  44688  fmtnoprmfac1lem  44689  fmtnoprmfac2lem1  44691  fmtnoprmfac2  44692  fmtnofac2lem  44693  2pwp1prm  44714  lighneallem1  44730  lighneallem4  44735  proththdlem  44738  proththd  44739  divgcdoddALTV  44807  perfectALTVlem1  44846  perfectALTVlem2  44847  perfectALTV  44848  gbowge7  44888  pw2m1lepw2m1  45534  nnolog2flm1  45609  dignn0fr  45620  dignn0flhalflem1  45634