Theorem 0zd 11266

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

Assertion

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

Proof of Theorem 0zd

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

Syntax hints:   → wi 4   ∈ wcel 1977  0cc0 9815  ℤcz 11254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-neg 10148  df-z 11255

This theorem is referenced by:  fzctr  12320  fzosubel3  12396  bcval5  12967  snopiswrd  13169  wrdsymb0  13194  ccatsymb  13219  swrdspsleq  13301  swrdccatin12lem2b  13337  swrdccat  13344  repswswrd  13382  eqwrds3  13552  fzomaxdiflem  13930  fsumzcl  14313  isumnn0nn  14413  climcndslem1  14420  climcnds  14422  harmonic  14430  geolim  14440  geolim2  14441  geoisum  14447  geoisumr  14448  mertenslem1  14455  mertenslem2  14456  mertens  14457  risefacval2  14580  fallfacval2  14581  binomfallfaclem2  14610  bpolydiflem  14624  eff  14651  efcvg  14654  reefcl  14656  efcj  14661  eftlub  14678  effsumlt  14680  eflegeo  14690  eirrlem  14771  ruclem6  14803  dvdsmod  14888  pwp1fsum  14952  bitsinv1lem  15001  sadcf  15013  sadadd3  15021  smupf  15038  alginv  15126  algcvg  15127  algcvga  15130  algfx  15131  eucalgcvga  15137  eucalg  15138  lcmftp  15187  phiprmpw  15319  fermltl  15327  iserodd  15378  pcpre1  15385  qexpz  15443  prmreclem4  15461  vdwapun  15516  odf1  17802  srgbinomlem4  18366  evlslem1  19336  cpmadugsumlemF  20500  dvnff  23492  dgrcl  23793  dgrub  23794  dgrlb  23796  elqaalem2  23879  elqaalem3  23880  geolim3  23898  tayl0  23920  dvtaylp  23928  radcnvlem1  23971  radcnvlem3  23973  radcnv0  23974  radcnvlt2  23977  pserulm  23980  psercn2  23981  pserdvlem2  23986  pserdv2  23988  abelthlem4  23992  abelthlem5  23993  abelthlem6  23994  abelthlem7  23996  abelthlem8  23997  abelthlem9  23998  cosne0  24080  logtayl  24206  leibpi  24469  leibpisum  24470  log2cnv  24471  log2tlbnd  24472  basellem3  24609  dchrptlem2  24790  bcmono  24802  lgslem4  24825  lgsne0  24860  numclwwlkovf2ex  26613  archiabllem1b  29077  oddpwdc  29743  ballotlemfval0  29884  fwddifnp1  31442  knoppcnlem6  31658  knoppcnlem9  31661  knoppcn  31664  knoppndvlem2  31674  knoppndvlem4  31676  knoppf  31696  itg2addnclem2  32632  rmynn  36541  jm2.24nn  36544  jm2.17c  36547  jm2.24  36548  acongrep  36565  acongeq  36568  jm2.18  36573  jm2.23  36581  jm2.20nn  36582  jm2.27a  36590  jm2.27c  36592  rmydioph  36599  hashnzfz  37541  bccbc  37566  binomcxplemnn0  37570  binomcxplemrat  37571  binomcxplemnotnn0  37577  mccllem  38664  expfac  38724  sinaover2ne0  38751  dvnmul  38833  dvnprodlem1  38836  dvnprodlem2  38837  stoweidlem11  38904  stoweidlem26  38919  stoweidlem34  38927  stirlinglem5  38971  fourierdlem11  39011  fourierdlem12  39012  fourierdlem14  39014  fourierdlem15  39015  fourierdlem24  39024  fourierdlem25  39025  fourierdlem36  39036  fourierdlem37  39037  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem64  39063  fourierdlem69  39068  fourierdlem73  39072  fourierdlem79  39078  fourierdlem81  39080  fourierdlem92  39091  fourierdlem93  39092  fourierdlem111  39110  elaa2lem  39126  etransclem3  39130  etransclem7  39134  etransclem10  39137  etransclem24  39151  etransclem27  39154  etransclem35  39162  etransclem44  39171  etransclem46  39173  etransclem47  39174  etransclem48  39175  iccpartigtl  39961  iccpartltu  39963  iccpartgt  39965  pfxnd  40258  pfxccatin12lem1  40286  2ffzoeq  40361  crctcsh1wlkn0lem3  41015  wwlksnextproplem1  41115  av-numclwwlkovf2ex  41517  0even  41721  2zrngamgm  41729  altgsumbcALT  41924  expnegico01  42102  dig0  42198  nn0sumshdiglem2  42214