Theorem 0zd 9224

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

Assertion

Ref	Expression
0zd	|- ( ph -> 0 e. ZZ )

Proof of Theorem 0zd

Step	Hyp	Ref	Expression
1		0z 9223	. 2 |- 0 e. ZZ
2	1	a1i 9	1 |- ( ph -> 0 e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2141   0cc0 7774   ZZcz 9212

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-1re 7868  ax-addrcl 7871  ax-rnegex 7883

This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-rab 2457  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-iota 5160  df-fv 5206  df-ov 5856  df-neg 8093  df-z 9213

This theorem is referenced by:  fzctr  10089  fzosubel3  10152  frecfzennn  10382  frechashgf1o  10384  0tonninf  10395  1tonninf  10396  exp3val  10478  exp0  10480  bcval  10683  bccmpl  10688  bcval5  10697  bcpasc  10700  bccl  10701  hashcl  10715  hashfiv01gt1  10716  hashfz1  10717  hashen  10718  fihashneq0  10729  omgadd  10737  fihashdom  10738  fiubz  10764  fnfz0hash  10767  ffzo0hash  10769  fzomaxdiflem  11076  fsumzcl  11365  fisum0diag  11404  fisum0diag2  11410  binomlem  11446  binom1dif  11450  isumnn0nn  11456  expcnvre  11466  explecnv  11468  pwm1geoserap1  11471  geolim  11474  geolim2  11475  geo2sum  11477  geoisum  11480  geoisumr  11481  mertenslemub  11497  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  fprod0diagfz  11591  eftcl  11617  efval  11624  eff  11626  efcvg  11629  efcvgfsum  11630  reefcl  11631  ege2le3  11634  efcj  11636  efaddlem  11637  eftlub  11653  effsumlt  11655  efgt1p2  11658  efgt1p  11659  eflegeo  11664  eirraplem  11739  dvdsmodexp  11757  dvdsmod  11822  gcdn0gt0  11933  gcdaddm  11939  gcdmultipled  11948  bezoutlemle  11963  nn0seqcvgd  11995  alginv  12001  algcvg  12002  algcvga  12005  algfx  12006  eucalgval2  12007  eucalgcvga  12012  eucalg  12013  lcmcllem  12021  lcmid  12034  mulgcddvds  12048  divgcdcoprmex  12056  cncongr1  12057  cncongr2  12058  phiprmpw  12176  modprm0  12208  pcpremul  12247  pceu  12249  pcmul  12255  pcqmul  12257  pcge0  12266  pcdvdsb  12273  pcneg  12278  pcgcd1  12281  pc2dvds  12283  pcz  12285  dvdsprmpweqle  12290  qexpz  12304  ennnfonelemjn  12357  ennnfonelemh  12359  ennnfonelem0  12360  ennnfonelem1  12362  ennnfonelemom  12363  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ennnfonelemex  12369  ennnfonelemrn  12374  ennnfonelemnn0  12377  ctinfomlemom  12382  lgsval  13699  lgsfvalg  13700  lgscllem  13702  lgsval2lem  13705  lgsneg1  13720  lgsne0  13733  012of  14028  2o01f  14029  isomninnlem  14062  iswomninnlem  14081  ismkvnnlem  14084  dceqnconst  14091  dcapnconst  14092