Theorem 0zd 12512

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

Syntax hints:   → wi 4   ∈ wcel 2114  0cc0 11038  ℤcz 12500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11096  ax-addrcl 11099  ax-rnegex 11109  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-neg 11379  df-z 12501

This theorem is referenced by:  fzctr  13568  fzosubel3  13654  bcval5  14253  snopiswrd  14458  wrdsymb0  14484  ccatsymb  14518  swrdspsleq  14601  pfxnd  14623  pfxccatin12lem1  14663  swrdccat  14670  repswswrd  14719  eqwrds3  14896  fzomaxdiflem  15278  fsumzcl  15670  isumnn0nn  15777  climcndslem1  15784  climcnds  15786  harmonic  15794  geolim  15805  geolim2  15806  geoisum  15812  geoisumr  15813  mertenslem1  15819  mertenslem2  15820  mertens  15821  risefacval2  15945  fallfacval2  15946  binomfallfaclem2  15975  bpolydiflem  15989  eff  16016  efcvg  16020  reefcl  16022  efcj  16027  eftlub  16046  effsumlt  16048  eflegeo  16058  eirrlem  16141  ruclem6  16172  dvdsmodexp  16199  dvdsmod  16268  pwp1fsum  16330  bitsinv1lem  16380  sadcf  16392  sadadd3  16400  smupf  16417  gcdmultipled  16473  alginv  16514  algcvg  16515  algcvga  16518  algfx  16519  eucalgcvga  16525  eucalg  16526  lcmftp  16575  phiprmpw  16715  iserodd  16775  pcpre1  16782  qexpz  16841  prmreclem4  16859  vdwapun  16914  chnpolfz  18568  smndex2dnrinv  18852  odf1  19503  ablsimpgfindlem1  20050  srgbinomlem4  20176  pzriprnglem5  21452  pzriprnglem8  21455  pzriprnglem10  21457  pzriprnglem11  21458  pzriprng1ALT  21463  evlslem1  22049  evlsvvvallem  22058  psdmul  22121  cpmadugsumlemF  22832  dvnff  25893  dgrcl  26206  dgrub  26207  dgrlb  26209  elqaalem2  26296  elqaalem3  26297  geolim3  26315  tayl0  26337  dvtaylp  26346  radcnvlem1  26390  radcnvlem3  26392  radcnv0  26393  radcnvlt2  26396  pserulm  26399  psercn2  26400  psercn2OLD  26401  pserdvlem2  26406  pserdv2  26408  abelthlem4  26412  abelthlem5  26413  abelthlem6  26414  abelthlem7  26416  abelthlem8  26417  abelthlem9  26418  cos02pilt1  26503  cosne0  26506  logtayl  26637  leibpi  26920  leibpisum  26921  log2cnv  26922  log2tlbnd  26923  basellem3  27061  dchrptlem2  27244  bcmono  27256  lgsne0  27314  crctcshwlkn0lem3  29897  fzo0opth  32893  pfxlsw2ccat  33042  wrdt2ind  33045  gsumzrsum  33158  gsummulgc2  33159  gsumwrd2dccatlem  33170  cycpmco2lem7  33225  cyc3conja  33250  archiabllem1b  33285  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnlem3  33337  elrgspnlem4  33338  elrgspnsubrunlem1  33340  elrgspnsubrunlem2  33341  esplyfval0  33740  esplyfval2  33741  esplympl  33743  esplyfval3  33748  vietadeg1  33754  constrrecl  33946  constrimcl  33947  constrmulcl  33948  constrreinvcl  33949  constrinvcl  33950  constrresqrtcl  33954  constrabscl  33955  constrsqrtcl  33956  cos9thpiminplylem1  33959  cos9thpiminplylem2  33960  cos9thpiminply  33965  cos9thpinconstrlem1  33966  oddpwdc  34531  ballotlemfval0  34673  fsum2dsub  34784  breprexplemc  34809  breprexp  34810  circlemeth  34817  fwddifnp1  36378  knoppcnlem6  36717  knoppcnlem9  36720  knoppcn  36723  knoppndvlem2  36732  knoppndvlem4  36734  knoppf  36754  itg2addnclem2  37920  lcmineqlem4  42399  lcmineqlem18  42413  aks4d1p1p2  42437  aks4d1p3  42445  aks4d1p7d1  42449  aks4d1p7  42450  aks4d1p8  42454  aks4d1p9  42455  posbezout  42467  primrootspoweq0  42473  aks6d1c1  42483  aks6d1c2lem4  42494  aks6d1c2  42497  aks6d1c5lem1  42503  aks6d1c5lem2  42505  2np3bcnp1  42511  sticksstones12a  42524  sticksstones22  42535  aks6d1c6lem3  42539  aks6d1c6lem4  42540  aks6d1c6isolem1  42541  aks6d1c6lem5  42544  bcled  42545  bcle2d  42546  aks6d1c7lem1  42547  aks6d1c7lem2  42548  psrbagres  42911  selvvvval  42940  evlselvlem  42941  evlselv  42942  mhphf  42952  fltnltalem  43017  rmynn  43310  jm2.24nn  43313  jm2.17c  43316  jm2.24  43317  acongrep  43334  acongeq  43337  jm2.18  43342  jm2.23  43350  jm2.20nn  43351  jm2.27a  43359  jm2.27c  43361  rmydioph  43368  hashnzfz  44673  bccbc  44698  binomcxplemnn0  44702  binomcxplemrat  44703  binomcxplemnotnn0  44709  mccllem  45954  expfac  46012  0cnv  46097  lmbr3v  46100  sinaover2ne0  46223  dvnmul  46298  dvnprodlem1  46301  dvnprodlem2  46302  stoweidlem11  46366  stoweidlem26  46381  stoweidlem34  46389  stirlinglem5  46433  fourierdlem11  46473  fourierdlem12  46474  fourierdlem14  46476  fourierdlem15  46477  fourierdlem24  46486  fourierdlem25  46487  fourierdlem36  46498  fourierdlem37  46499  fourierdlem41  46503  fourierdlem48  46509  fourierdlem49  46510  fourierdlem50  46511  fourierdlem64  46525  fourierdlem69  46530  fourierdlem73  46534  fourierdlem79  46540  fourierdlem81  46542  fourierdlem92  46553  fourierdlem93  46554  fourierdlem111  46572  elaa2lem  46588  etransclem3  46592  etransclem7  46596  etransclem10  46599  etransclem24  46613  etransclem27  46616  etransclem35  46624  etransclem44  46633  etransclem46  46635  etransclem47  46636  etransclem48  46637  natglobalincr  47232  chnsubseqwl  47234  chnsubseq  47235  2ffzoeq  47684  iccpartigtl  47780  iccpartltu  47782  iccpartgt  47784  0even  48594  2zrngamgm  48602  altgsumbcALT  48710  expnegico01  48875  dig0  48963  nn0sumshdiglem2  48979