Theorem 0zd 12651

Description: Zero is an integer, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
0zd	⊢ (𝜑 → 0 ∈ ℤ)

Proof of Theorem 0zd

Step	Hyp	Ref	Expression
1		0z 12650	. 2 ⊢ 0 ∈ ℤ
2	1	a1i 11	1 ⊢ (𝜑 → 0 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2108  0cc0 11184  ℤcz 12639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-addrcl 11245  ax-rnegex 11255  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-neg 11523  df-z 12640

This theorem is referenced by:  fzctr  13697  fzosubel3  13777  bcval5  14367  snopiswrd  14571  wrdsymb0  14597  ccatsymb  14630  swrdspsleq  14713  pfxnd  14735  pfxccatin12lem1  14776  swrdccat  14783  repswswrd  14832  eqwrds3  15010  fzomaxdiflem  15391  fsumzcl  15783  isumnn0nn  15890  climcndslem1  15897  climcnds  15899  harmonic  15907  geolim  15918  geolim2  15919  geoisum  15925  geoisumr  15926  mertenslem1  15932  mertenslem2  15933  mertens  15934  risefacval2  16058  fallfacval2  16059  binomfallfaclem2  16088  bpolydiflem  16102  eff  16129  efcvg  16133  reefcl  16135  efcj  16140  eftlub  16157  effsumlt  16159  eflegeo  16169  eirrlem  16252  ruclem6  16283  dvdsmodexp  16310  dvdsmod  16377  pwp1fsum  16439  bitsinv1lem  16487  sadcf  16499  sadadd3  16507  smupf  16524  gcdmultipled  16581  alginv  16622  algcvg  16623  algcvga  16626  algfx  16627  eucalgcvga  16633  eucalg  16634  lcmftp  16683  phiprmpw  16823  iserodd  16882  pcpre1  16889  qexpz  16948  prmreclem4  16966  vdwapun  17021  smndex2dnrinv  18950  odf1  19604  ablsimpgfindlem1  20151  srgbinomlem4  20256  pzriprnglem5  21519  pzriprnglem8  21522  pzriprnglem10  21524  pzriprnglem11  21525  pzriprng1ALT  21530  evlslem1  22129  psdmul  22193  cpmadugsumlemF  22903  dvnff  25979  dgrcl  26292  dgrub  26293  dgrlb  26295  elqaalem2  26380  elqaalem3  26381  geolim3  26399  tayl0  26421  dvtaylp  26430  radcnvlem1  26474  radcnvlem3  26476  radcnv0  26477  radcnvlt2  26480  pserulm  26483  psercn2  26484  psercn2OLD  26485  pserdvlem2  26490  pserdv2  26492  abelthlem4  26496  abelthlem5  26497  abelthlem6  26498  abelthlem7  26500  abelthlem8  26501  abelthlem9  26502  cos02pilt1  26586  cosne0  26589  logtayl  26720  leibpi  27003  leibpisum  27004  log2cnv  27005  log2tlbnd  27006  basellem3  27144  dchrptlem2  27327  bcmono  27339  lgsne0  27397  crctcshwlkn0lem3  29845  fzo0opth  32810  pfxlsw2ccat  32917  wrdt2ind  32920  cycpmco2lem7  33125  cyc3conja  33150  archiabllem1b  33172  oddpwdc  34319  ballotlemfval0  34460  fsum2dsub  34584  breprexplemc  34609  breprexp  34610  circlemeth  34617  fwddifnp1  36129  knoppcnlem6  36464  knoppcnlem9  36467  knoppcn  36470  knoppndvlem2  36479  knoppndvlem4  36481  knoppf  36501  itg2addnclem2  37632  lcmineqlem4  41989  lcmineqlem18  42003  aks4d1p1p2  42027  aks4d1p3  42035  aks4d1p7d1  42039  aks4d1p7  42040  aks4d1p8  42044  aks4d1p9  42045  posbezout  42057  primrootspoweq0  42063  aks6d1c1  42073  aks6d1c2lem4  42084  aks6d1c2  42087  aks6d1c5lem1  42093  aks6d1c5lem2  42095  2np3bcnp1  42101  sticksstones12a  42114  sticksstones22  42125  aks6d1c6lem3  42129  aks6d1c6lem4  42130  aks6d1c6isolem1  42131  aks6d1c6lem5  42134  bcled  42135  bcle2d  42136  aks6d1c7lem1  42137  aks6d1c7lem2  42138  metakunt29  42190  metakunt30  42191  metakunt32  42193  metakunt33  42194  psrbagres  42501  evlsvvvallem  42516  selvvvval  42540  evlselvlem  42541  evlselv  42542  mhphf  42552  fltnltalem  42617  rmynn  42913  jm2.24nn  42916  jm2.17c  42919  jm2.24  42920  acongrep  42937  acongeq  42940  jm2.18  42945  jm2.23  42953  jm2.20nn  42954  jm2.27a  42962  jm2.27c  42964  rmydioph  42971  hashnzfz  44289  bccbc  44314  binomcxplemnn0  44318  binomcxplemrat  44319  binomcxplemnotnn0  44325  mccllem  45518  expfac  45578  0cnv  45663  lmbr3v  45666  sinaover2ne0  45789  dvnmul  45864  dvnprodlem1  45867  dvnprodlem2  45868  stoweidlem11  45932  stoweidlem26  45947  stoweidlem34  45955  stirlinglem5  45999  fourierdlem11  46039  fourierdlem12  46040  fourierdlem14  46042  fourierdlem15  46043  fourierdlem24  46052  fourierdlem25  46053  fourierdlem36  46064  fourierdlem37  46065  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem64  46091  fourierdlem69  46096  fourierdlem73  46100  fourierdlem79  46106  fourierdlem81  46108  fourierdlem92  46119  fourierdlem93  46120  fourierdlem111  46138  elaa2lem  46154  etransclem3  46158  etransclem7  46162  etransclem10  46165  etransclem24  46179  etransclem27  46182  etransclem35  46190  etransclem44  46199  etransclem46  46201  etransclem47  46202  etransclem48  46203  natglobalincr  46796  2ffzoeq  47242  iccpartigtl  47297  iccpartltu  47299  iccpartgt  47301  0even  47960  2zrngamgm  47968  altgsumbcALT  48078  expnegico01  48247  dig0  48340  nn0sumshdiglem2  48356