Theorem 0zd 9199

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

Syntax hints:   → wi 4   ∈ wcel 2136  0cc0 7749  ℤcz 9187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-1re 7843  ax-addrcl 7846  ax-rnegex 7858

This theorem depends on definitions:  df-bi 116  df-3or 969  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-ral 2448  df-rex 2449  df-rab 2452  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195  df-ov 5844  df-neg 8068  df-z 9188

This theorem is referenced by:  fzctr  10064  fzosubel3  10127  frecfzennn  10357  frechashgf1o  10359  0tonninf  10370  1tonninf  10371  exp3val  10453  exp0  10455  bcval  10658  bccmpl  10663  bcval5  10672  bcpasc  10675  bccl  10676  hashcl  10690  hashfiv01gt1  10691  hashfz1  10692  hashen  10693  fihashneq0  10704  omgadd  10711  fihashdom  10712  fiubz  10738  fnfz0hash  10741  ffzo0hash  10743  fzomaxdiflem  11050  fsumzcl  11339  fisum0diag  11378  fisum0diag2  11384  binomlem  11420  binom1dif  11424  isumnn0nn  11430  expcnvre  11440  explecnv  11442  pwm1geoserap1  11445  geolim  11448  geolim2  11449  geo2sum  11451  geoisum  11454  geoisumr  11455  mertenslemub  11471  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  fprod0diagfz  11565  eftcl  11591  efval  11598  eff  11600  efcvg  11603  efcvgfsum  11604  reefcl  11605  ege2le3  11608  efcj  11610  efaddlem  11611  eftlub  11627  effsumlt  11629  efgt1p2  11632  efgt1p  11633  eflegeo  11638  eirraplem  11713  dvdsmodexp  11731  dvdsmod  11796  gcdn0gt0  11907  gcdaddm  11913  gcdmultipled  11922  bezoutlemle  11937  nn0seqcvgd  11969  alginv  11975  algcvg  11976  algcvga  11979  algfx  11980  eucalgval2  11981  eucalgcvga  11986  eucalg  11987  lcmcllem  11995  lcmid  12008  mulgcddvds  12022  divgcdcoprmex  12030  cncongr1  12031  cncongr2  12032  phiprmpw  12150  modprm0  12182  pcpremul  12221  pceu  12223  pcmul  12229  pcqmul  12231  pcge0  12240  pcdvdsb  12247  pcneg  12252  pcgcd1  12255  pc2dvds  12257  pcz  12259  dvdsprmpweqle  12264  qexpz  12278  ennnfonelemjn  12331  ennnfonelemh  12333  ennnfonelem0  12334  ennnfonelem1  12336  ennnfonelemom  12337  ennnfonelemkh  12341  ennnfonelemhf1o  12342  ennnfonelemex  12343  ennnfonelemrn  12348  ennnfonelemnn0  12351  ctinfomlemom  12356  lgsval  13505  lgsfvalg  13506  lgscllem  13508  lgsval2lem  13511  lgsneg1  13526  lgsne0  13539  012of  13835  2o01f  13836  isomninnlem  13869  iswomninnlem  13888  ismkvnnlem  13891  dceqnconst  13898  dcapnconst  13899