Theorem 0zd 9386

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 9385	. 2 |- 0 e. ZZ
2	1	a1i 9	1 |- ( ph -> 0 e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2176   0cc0 7927   ZZcz 9374

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-1re 8021  ax-addrcl 8024  ax-rnegex 8036

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-rab 2493  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280  df-ov 5949  df-neg 8248  df-z 9375

This theorem is referenced by:  fzctr  10257  fzosubel3  10327  frecfzennn  10573  frechashgf1o  10575  0tonninf  10587  1tonninf  10588  exp3val  10688  exp0  10690  bcval  10896  bccmpl  10901  bcval5  10910  bcpasc  10913  bccl  10914  hashcl  10928  hashfiv01gt1  10929  hashfz1  10930  hashen  10931  fihashneq0  10941  omgadd  10949  fihashdom  10950  fiubz  10976  fnfz0hash  10979  ffzo0hash  10981  wrdval  10999  snopiswrd  11006  wrdsymb0  11028  ccatfvalfi  11051  ccatcl  11052  ccatlen  11054  ccatsymb  11061  fzowrddc  11103  swrdval  11104  swrdspsleq  11123  pfxval  11130  pfxclg  11133  pfxnd  11143  pfxwrdsymbg  11144  fzomaxdiflem  11456  fsumzcl  11746  fisum0diag  11785  fisum0diag2  11791  binomlem  11827  binom1dif  11831  isumnn0nn  11837  expcnvre  11847  explecnv  11849  pwm1geoserap1  11852  geolim  11855  geolim2  11856  geo2sum  11858  geoisum  11861  geoisumr  11862  mertenslemub  11878  mertenslemi1  11879  mertenslem2  11880  mertensabs  11881  fprod0diagfz  11972  eftcl  11998  efval  12005  eff  12007  efcvg  12010  efcvgfsum  12011  reefcl  12012  ege2le3  12015  efcj  12017  efaddlem  12018  eftlub  12034  effsumlt  12036  efgt1p2  12039  efgt1p  12040  eflegeo  12045  eirraplem  12121  dvdsmodexp  12139  dvdsmod  12206  3dvds  12208  bitsfzolem  12298  bitsfi  12301  bitsinv1lem  12305  bitsinv1  12306  gcdn0gt0  12332  gcdaddm  12338  gcdmultipled  12347  bezoutlemle  12362  nninfctlemfo  12394  nn0seqcvgd  12396  alginv  12402  algcvg  12403  algcvga  12406  algfx  12407  eucalgval2  12408  eucalgcvga  12413  eucalg  12414  lcmcllem  12422  lcmid  12435  mulgcddvds  12449  divgcdcoprmex  12457  cncongr1  12458  cncongr2  12459  phiprmpw  12577  modprm0  12610  pcpremul  12649  pceu  12651  pcmul  12657  pcqmul  12659  pcge0  12669  pcdvdsb  12676  pcneg  12681  pcgcd1  12684  pc2dvds  12686  pcz  12688  dvdsprmpweqle  12693  qexpz  12708  4sqlemafi  12751  4sqlem11  12757  ennnfonelemjn  12806  ennnfonelemh  12808  ennnfonelem0  12809  ennnfonelem1  12811  ennnfonelemom  12812  ennnfonelemkh  12816  ennnfonelemhf1o  12817  ennnfonelemex  12818  ennnfonelemrn  12823  ennnfonelemnn0  12826  ctinfomlemom  12831  mulgval  13491  mulgfng  13493  subgmulg  13557  elply2  15240  plyf  15242  elplyd  15246  ply1termlem  15247  plyaddlem1  15252  plymullem1  15253  plymullem  15255  plycoeid3  15262  plycolemc  15263  plycjlemc  15265  plycn  15267  plyrecj  15268  dvply1  15270  sgmppw  15497  0sgmppw  15498  mersenne  15502  lgsval  15514  lgsfvalg  15515  lgscllem  15517  lgsval2lem  15520  lgsneg1  15535  lgsne0  15548  lgsquad3  15594  012of  15967  2o01f  15968  isomninnlem  16006  iswomninnlem  16025  ismkvnnlem  16028  dceqnconst  16036  dcapnconst  16037