Theorem nnzd 12434

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℕcn 11982  ℤcz 12328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353  ax-un 7597  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-i2m1 10948  ax-1ne0 10949  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  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 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-om 7722  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-neg 11217  df-nn 11983  df-n0 12243  df-z 12329

This theorem is referenced by:  expaddzlem  13835  expmulz  13838  expmulnbnd  13959  facndiv  14011  bcval5  14041  bcpasc  14044  hashf1  14180  isercolllem1  15385  isercolllem2  15386  o1fsum  15534  bcxmas  15556  climcndslem2  15571  climcnds  15572  mertenslem1  15605  fprodser  15668  bpolydiflem  15773  eftlub  15827  eirrlem  15922  rpnnen2lem7  15938  rpnnen2lem9  15940  rpnnen2lem11  15942  sqrt2irrlem  15966  dvdsfac  16044  dvdsmod  16047  oddpwp1fsum  16110  bitsfzolem  16150  bitsmod  16152  bitsfi  16153  bitscmp  16154  bitsinv1  16158  sadadd3  16177  sadaddlem  16182  bitsuz  16190  bitsshft  16191  gcdnncl  16223  gcd1  16244  dvdsgcdidd  16254  bezoutlem3  16258  bezoutlem4  16259  mulgcd  16265  gcdmultiplezOLD  16270  rplpwr  16276  rprpwr  16277  sqgcd  16279  dvdssq  16281  lcmneg  16317  lcmgcdlem  16320  rpdvds  16374  coprmprod  16375  coprmproddvdslem  16376  congr  16378  cncongr1  16381  cncongr2  16382  prmz  16389  prmind2  16399  divgcdodd  16424  isprm6  16428  prmexpb  16434  prmfac1  16435  rpexp  16436  prmdvdsncoprmbd  16440  numdensq  16467  hashdvds  16485  phiprmpw  16486  crth  16488  phimullem  16489  eulerthlem1  16491  eulerthlem2  16492  prmdivdiv  16497  hashgcdlem  16498  odzdvds  16505  pythagtriplem4  16529  pythagtriplem6  16531  pythagtriplem7  16532  pythagtriplem11  16535  pythagtriplem13  16537  pythagtriplem19  16543  pclem  16548  pcprendvds2  16551  pcpre1  16552  pcpremul  16553  pceulem  16555  pcqmul  16563  pcdvdsb  16579  pcidlem  16582  pcdvdstr  16586  pcgcd1  16587  pc2dvds  16589  pcprmpw2  16592  pcaddlem  16598  pcadd  16599  pcmpt2  16603  pcmptdvds  16604  pcfac  16609  pcbc  16610  qexpz  16611  oddprmdvds  16613  prmpwdvds  16614  pockthlem  16615  pockthg  16616  prmreclem2  16627  prmreclem3  16628  prmreclem4  16629  prmreclem5  16630  prmreclem6  16631  4sqlem5  16652  4sqlem8  16655  4sqlem9  16656  4sqlem10  16657  4sqlem12  16666  4sqlem14  16668  4sqlem16  16670  4sqlem17  16671  vdwlem1  16691  vdwlem2  16692  vdwlem3  16693  vdwlem6  16696  vdwlem9  16699  vdwlem10  16700  vdwnnlem3  16707  prmdvdsprmop  16753  prmolelcmf  16758  prmgaplem1  16759  prmgaplem7  16767  prmgaplem8  16768  gsumwsubmcl  18484  gsumsgrpccat  18487  gsumccatOLD  18488  gsumwmhm  18493  mulgneg  18731  mulgnndir  18741  psgnunilem4  19114  odlem2  19156  mndodconglem  19158  odmod  19163  gexlem2  19196  gexcl3  19201  gexcl2  19203  sylow1lem1  19212  sylow1lem3  19214  sylow1lem5  19216  pgpfi  19219  fislw  19239  sylow3lem4  19244  gexexlem  19462  ablfacrplem  19677  ablfacrp  19678  ablfacrp2  19679  ablfac1lem  19680  ablfac1b  19682  ablfac1eu  19685  pgpfac1lem3a  19688  ablfaclem3  19699  fincygsubgd  19723  fincygsubgodd  19724  znrrg  20782  cayhamlem1  22024  caublcls  24482  ovolicc2lem4  24693  iundisj2  24722  volsup  24729  uniioombllem3  24758  mbfi1fseqlem3  24891  mbfi1fseqlem4  24892  elqaalem2  25489  aalioulem1  25501  aalioulem4  25504  aalioulem5  25505  aalioulem6  25506  aaliou  25507  aaliou3lem1  25511  aaliou3lem2  25512  aaliou3lem3  25513  aaliou3lem8  25514  aaliou3lem5  25516  aaliou3lem6  25517  aaliou3lem7  25518  taylthlem2  25542  cxpeq  25919  amgmlem  26148  lgamgulmlem4  26190  lgamcvg2  26213  wilthlem2  26227  wilth  26229  wilthimp  26230  ftalem5  26235  basellem2  26240  basellem3  26241  basellem4  26242  basellem5  26243  muval1  26291  dvdssqf  26296  sgmnncl  26305  efchtdvds  26317  mumullem2  26338  mumul  26339  sqff1o  26340  fsumdvdsdiaglem  26341  dvdsppwf1o  26344  dvdsflf1o  26345  muinv  26351  dvdsmulf1o  26352  chtublem  26368  fsumvma2  26371  vmasum  26373  chpchtsum  26376  logfacubnd  26378  mersenne  26384  perfect1  26385  perfectlem1  26386  perfectlem2  26387  perfect  26388  dchrelbas4  26400  dchrfi  26412  bcmono  26434  bcp1ctr  26436  bclbnd  26437  bposlem1  26441  bposlem3  26443  bposlem5  26445  bposlem6  26446  bposlem9  26449  lgsmod  26480  lgsdir  26489  lgsdilem2  26490  lgsne0  26492  lgsqrlem2  26504  lgsqr  26508  lgsqrmodndvds  26510  gausslemma2dlem0c  26515  gausslemma2dlem0h  26520  gausslemma2dlem0i  26521  gausslemma2dlem2  26524  gausslemma2dlem6  26529  gausslemma2dlem7  26530  gausslemma2d  26531  lgseisenlem1  26532  lgseisenlem2  26533  lgseisenlem3  26534  lgseisenlem4  26535  lgsquadlem1  26537  lgsquadlem2  26538  lgsquadlem3  26539  lgsquad2lem1  26541  lgsquad2lem2  26542  lgsquad2  26543  m1lgs  26545  2lgslem2  26552  2sqlem3  26577  2sqlem4  26578  2sqlem8  26583  chebbnd1lem1  26626  rplogsumlem2  26642  rpvmasumlem  26644  dchrisumlem1  26646  dchrisumlem2  26647  dchrisumlem3  26648  dchrisum0fmul  26663  dchrisum0ff  26664  dchrisum0flblem1  26665  dchrisum0flblem2  26666  dchrisum0flb  26667  dchrisum0  26677  pntrsumbnd2  26724  pntrlog2bndlem1  26734  pntrlog2bndlem6  26740  pntpbnd2  26744  pntlemg  26755  pntlemj  26760  pntlemf  26762  ostth2lem2  26791  ostth2lem3  26792  ostth3  26795  numclwlk2lem2f1o  28752  minvecolem4  29251  iundisj2f  30938  ssnnssfz  31117  iundisj2fi  31127  f1ocnt  31132  prmdvdsbc  31139  numdenneg  31140  ltesubnnd  31145  psgnfzto1stlem  31376  isarchi3  31450  archiabllem1b  31455  smatrcl  31755  1smat1  31763  submateqlem1  31766  lmatfvlem  31774  qqhval2  31941  qqhf  31945  qqhghm  31947  qqhrhm  31948  qqhnm  31949  qqhre  31979  esumcvg  32063  meascnbl  32196  omssubadd  32276  oddpwdc  32330  ballotlemfp1  32467  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemimin  32481  ballotlemic  32482  ballotlem1c  32483  hgt750lemc  32636  hgt750lemd  32637  hgt750lemb  32645  hgt750leme  32647  subfaclim  33159  cvmliftlem7  33262  sinccvglem  33639  bcprod  33713  bccolsum  33714  faclimlem2  33719  faclim2  33723  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem6  35792  poimirlem8  35794  poimirlem9  35795  poimirlem10  35796  poimirlem11  35797  poimirlem13  35799  poimirlem14  35800  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem18  35804  poimirlem19  35805  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem23  35809  poimirlem24  35810  poimirlem26  35812  poimirlem27  35813  poimirlem28  35814  poimirlem31  35817  mblfinlem2  35824  seqpo  35914  incsequz  35915  incsequz2  35916  bccl2d  40007  nnproddivdvdsd  40016  lcmineqlem1  40044  lcmineqlem3  40046  lcmineqlem4  40047  lcmineqlem6  40049  lcmineqlem8  40051  lcmineqlem9  40052  lcmineqlem10  40053  lcmineqlem11  40054  lcmineqlem13  40056  lcmineqlem14  40057  lcmineqlem18  40061  lcmineqlem19  40062  lcmineqlem20  40063  lcmineqlem21  40064  lcmineqlem22  40065  lcmineqlem23  40066  lcmineqlem  40067  3lexlogpow5ineq2  40070  3lexlogpow2ineq1  40073  aks4d1p3  40093  aks4d1p5  40095  aks4d1p6  40096  aks4d1p8d1  40099  aks4d1p8d2  40100  aks4d1p8d3  40101  aks4d1p8  40102  aks4d1p9  40103  sticksstones6  40114  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  metakunt1  40132  metakunt2  40133  metakunt3  40134  metakunt4  40135  metakunt5  40136  metakunt7  40138  metakunt10  40141  metakunt15  40146  metakunt16  40147  metakunt18  40149  metakunt19  40150  metakunt20  40151  metakunt21  40152  metakunt22  40153  metakunt24  40155  metakunt25  40156  metakunt26  40157  metakunt27  40158  metakunt28  40159  metakunt29  40160  metakunt30  40161  metakunt32  40163  metakunt33  40164  oexpreposd  40328  exp11d  40332  gcdle1d  40337  gcdle2d  40338  expgcd  40341  nn0expgcd  40342  numdenexp  40344  dvdsexpnn0  40348  zrtelqelz  40352  fltdvdsabdvdsc  40482  fltaccoprm  40484  fltbccoprm  40485  fltabcoprm  40486  fltne  40488  flt4lem2  40491  flt4lem3  40492  flt4lem4  40493  flt4lem5  40494  flt4lem5elem  40495  flt4lem5a  40496  flt4lem5b  40497  flt4lem5c  40498  flt4lem5d  40499  flt4lem5e  40500  flt4lem5f  40501  flt4lem6  40502  flt4lem7  40503  nna4b4nsq  40504  fltltc  40505  fltnlta  40507  irrapxlem3  40653  irrapxlem5  40655  pellexlem5  40662  pellexlem6  40663  pellex  40664  pell1234qrmulcl  40684  jm2.23  40825  jm2.20nn  40826  jm2.26lem3  40830  jm2.27a  40834  jm2.27b  40835  jm2.27c  40836  jm3.1lem1  40846  jm3.1lem3  40848  inductionexd  41772  nznngen  41941  hashnzfz2  41946  fmuldfeq  43131  divcnvg  43175  stoweidlem1  43549  stoweidlem3  43551  stoweidlem11  43559  stoweidlem20  43568  stoweidlem26  43574  stoweidlem34  43582  stoweidlem51  43599  stirlinglem4  43625  stirlinglem5  43626  stirlinglem8  43629  dirkerper  43644  dirkertrigeqlem2  43647  dirkertrigeqlem3  43648  dirkercncflem2  43652  fourierdlem11  43666  fourierdlem14  43669  fourierdlem20  43675  fourierdlem25  43680  fourierdlem37  43692  fourierdlem41  43696  fourierdlem48  43702  fourierdlem49  43703  fourierdlem54  43708  fourierdlem64  43718  fourierdlem73  43727  fourierdlem79  43733  fourierdlem92  43746  fourierdlem93  43747  fourierdlem111  43765  sqwvfourb  43777  etransclem3  43785  etransclem7  43789  etransclem10  43792  etransclem15  43797  etransclem24  43806  etransclem25  43807  etransclem26  43808  etransclem27  43809  etransclem28  43810  etransclem35  43817  etransclem37  43819  etransclem38  43820  etransclem41  43823  etransclem44  43826  etransclem45  43827  etransclem48  43830  ovnsubaddlem1  44115  vonioolem1  44225  iccpartgtprec  44883  iccpartipre  44884  fmtnoodd  44996  goldbachthlem2  45009  goldbachth  45010  odz2prm2pw  45026  fmtnoprmfac1lem  45027  fmtnoprmfac2lem1  45029  fmtnoprmfac2  45030  fmtnofac2lem  45031  2pwp1prm  45052  lighneallem1  45068  lighneallem4  45073  proththdlem  45076  proththd  45077  divgcdoddALTV  45145  perfectALTVlem1  45184  perfectALTVlem2  45185  perfectALTV  45186  gbowge7  45226  pw2m1lepw2m1  45872  nnolog2flm1  45947  dignn0fr  45958  dignn0flhalflem1  45972