Theorem 0zd 12622

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 12621	. 2 ⊢ 0 ∈ ℤ
2	1	a1i 11	1 ⊢ (𝜑 → 0 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2105  0cc0 11152  ℤcz 12610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-addrcl 11213  ax-rnegex 11223  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-neg 11492  df-z 12611

This theorem is referenced by:  fzctr  13676  fzosubel3  13761  bcval5  14353  snopiswrd  14557  wrdsymb0  14583  ccatsymb  14616  swrdspsleq  14699  pfxnd  14721  pfxccatin12lem1  14762  swrdccat  14769  repswswrd  14818  eqwrds3  14996  fzomaxdiflem  15377  fsumzcl  15767  isumnn0nn  15874  climcndslem1  15881  climcnds  15883  harmonic  15891  geolim  15902  geolim2  15903  geoisum  15909  geoisumr  15910  mertenslem1  15916  mertenslem2  15917  mertens  15918  risefacval2  16042  fallfacval2  16043  binomfallfaclem2  16072  bpolydiflem  16086  eff  16113  efcvg  16117  reefcl  16119  efcj  16124  eftlub  16141  effsumlt  16143  eflegeo  16153  eirrlem  16236  ruclem6  16267  dvdsmodexp  16294  dvdsmod  16362  pwp1fsum  16424  bitsinv1lem  16474  sadcf  16486  sadadd3  16494  smupf  16511  gcdmultipled  16567  alginv  16608  algcvg  16609  algcvga  16612  algfx  16613  eucalgcvga  16619  eucalg  16620  lcmftp  16669  phiprmpw  16809  iserodd  16868  pcpre1  16875  qexpz  16934  prmreclem4  16952  vdwapun  17007  smndex2dnrinv  18940  odf1  19594  ablsimpgfindlem1  20141  srgbinomlem4  20246  pzriprnglem5  21513  pzriprnglem8  21516  pzriprnglem10  21518  pzriprnglem11  21519  pzriprng1ALT  21524  evlslem1  22123  psdmul  22187  cpmadugsumlemF  22897  dvnff  25973  dgrcl  26286  dgrub  26287  dgrlb  26289  elqaalem2  26376  elqaalem3  26377  geolim3  26395  tayl0  26417  dvtaylp  26426  radcnvlem1  26470  radcnvlem3  26472  radcnv0  26473  radcnvlt2  26476  pserulm  26479  psercn2  26480  psercn2OLD  26481  pserdvlem2  26486  pserdv2  26488  abelthlem4  26492  abelthlem5  26493  abelthlem6  26494  abelthlem7  26496  abelthlem8  26497  abelthlem9  26498  cos02pilt1  26582  cosne0  26585  logtayl  26716  leibpi  26999  leibpisum  27000  log2cnv  27001  log2tlbnd  27002  basellem3  27140  dchrptlem2  27323  bcmono  27335  lgsne0  27393  crctcshwlkn0lem3  29841  fzo0opth  32812  pfxlsw2ccat  32919  wrdt2ind  32922  gsumzrsum  33044  gsummulgc2  33045  gsumwrd2dccatlem  33051  cycpmco2lem7  33134  cyc3conja  33159  archiabllem1b  33181  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem3  33233  elrgspnlem4  33234  oddpwdc  34335  ballotlemfval0  34476  fsum2dsub  34600  breprexplemc  34625  breprexp  34626  circlemeth  34633  fwddifnp1  36146  knoppcnlem6  36480  knoppcnlem9  36483  knoppcn  36486  knoppndvlem2  36495  knoppndvlem4  36497  knoppf  36517  itg2addnclem2  37658  lcmineqlem4  42013  lcmineqlem18  42027  aks4d1p1p2  42051  aks4d1p3  42059  aks4d1p7d1  42063  aks4d1p7  42064  aks4d1p8  42068  aks4d1p9  42069  posbezout  42081  primrootspoweq0  42087  aks6d1c1  42097  aks6d1c2lem4  42108  aks6d1c2  42111  aks6d1c5lem1  42117  aks6d1c5lem2  42119  2np3bcnp1  42125  sticksstones12a  42138  sticksstones22  42149  aks6d1c6lem3  42153  aks6d1c6lem4  42154  aks6d1c6isolem1  42155  aks6d1c6lem5  42158  bcled  42159  bcle2d  42160  aks6d1c7lem1  42161  aks6d1c7lem2  42162  metakunt29  42214  metakunt30  42215  metakunt32  42217  metakunt33  42218  psrbagres  42532  evlsvvvallem  42547  selvvvval  42571  evlselvlem  42572  evlselv  42573  mhphf  42583  fltnltalem  42648  rmynn  42944  jm2.24nn  42947  jm2.17c  42950  jm2.24  42951  acongrep  42968  acongeq  42971  jm2.18  42976  jm2.23  42984  jm2.20nn  42985  jm2.27a  42993  jm2.27c  42995  rmydioph  43002  hashnzfz  44315  bccbc  44340  binomcxplemnn0  44344  binomcxplemrat  44345  binomcxplemnotnn0  44351  mccllem  45552  expfac  45612  0cnv  45697  lmbr3v  45700  sinaover2ne0  45823  dvnmul  45898  dvnprodlem1  45901  dvnprodlem2  45902  stoweidlem11  45966  stoweidlem26  45981  stoweidlem34  45989  stirlinglem5  46033  fourierdlem11  46073  fourierdlem12  46074  fourierdlem14  46076  fourierdlem15  46077  fourierdlem24  46086  fourierdlem25  46087  fourierdlem36  46098  fourierdlem37  46099  fourierdlem41  46103  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem64  46125  fourierdlem69  46130  fourierdlem73  46134  fourierdlem79  46140  fourierdlem81  46142  fourierdlem92  46153  fourierdlem93  46154  fourierdlem111  46172  elaa2lem  46188  etransclem3  46192  etransclem7  46196  etransclem10  46199  etransclem24  46213  etransclem27  46216  etransclem35  46224  etransclem44  46233  etransclem46  46235  etransclem47  46236  etransclem48  46237  natglobalincr  46830  2ffzoeq  47276  iccpartigtl  47347  iccpartltu  47349  iccpartgt  47351  0even  48080  2zrngamgm  48088  altgsumbcALT  48197  expnegico01  48363  dig0  48455  nn0sumshdiglem2  48471