Theorem 0zd 9419

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

Syntax hints:   -> wi 4   e. wcel 2178   0cc0 7960   ZZcz 9407

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-1re 8054  ax-addrcl 8057  ax-rnegex 8069

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-rab 2495  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970  df-neg 8281  df-z 9408

This theorem is referenced by:  fzctr  10290  fzosubel3  10362  frecfzennn  10608  frechashgf1o  10610  0tonninf  10622  1tonninf  10623  exp3val  10723  exp0  10725  bcval  10931  bccmpl  10936  bcval5  10945  bcpasc  10948  bccl  10949  hashcl  10963  hashfiv01gt1  10964  hashfz1  10965  hashen  10966  fihashneq0  10976  omgadd  10984  fihashdom  10985  fiubz  11011  fnfz0hash  11014  ffzo0hash  11016  wrdval  11034  snopiswrd  11041  wrdsymb0  11063  ccatfvalfi  11086  ccatcl  11087  ccatlen  11089  ccatsymb  11096  fzowrddc  11138  swrdval  11139  swrdspsleq  11158  pfxval  11165  fnpfx  11168  pfxclg  11169  pfxnd  11180  pfxwrdsymbg  11181  pfxccatin12lem1  11219  pfxccatin12  11224  swrdccat  11226  fzomaxdiflem  11538  fsumzcl  11828  fisum0diag  11867  fisum0diag2  11873  binomlem  11909  binom1dif  11913  isumnn0nn  11919  expcnvre  11929  explecnv  11931  pwm1geoserap1  11934  geolim  11937  geolim2  11938  geo2sum  11940  geoisum  11943  geoisumr  11944  mertenslemub  11960  mertenslemi1  11961  mertenslem2  11962  mertensabs  11963  fprod0diagfz  12054  eftcl  12080  efval  12087  eff  12089  efcvg  12092  efcvgfsum  12093  reefcl  12094  ege2le3  12097  efcj  12099  efaddlem  12100  eftlub  12116  effsumlt  12118  efgt1p2  12121  efgt1p  12122  eflegeo  12127  eirraplem  12203  dvdsmodexp  12221  dvdsmod  12288  3dvds  12290  bitsfzolem  12380  bitsfi  12383  bitsinv1lem  12387  bitsinv1  12388  gcdn0gt0  12414  gcdaddm  12420  gcdmultipled  12429  bezoutlemle  12444  nninfctlemfo  12476  nn0seqcvgd  12478  alginv  12484  algcvg  12485  algcvga  12488  algfx  12489  eucalgval2  12490  eucalgcvga  12495  eucalg  12496  lcmcllem  12504  lcmid  12517  mulgcddvds  12531  divgcdcoprmex  12539  cncongr1  12540  cncongr2  12541  phiprmpw  12659  modprm0  12692  pcpremul  12731  pceu  12733  pcmul  12739  pcqmul  12741  pcge0  12751  pcdvdsb  12758  pcneg  12763  pcgcd1  12766  pc2dvds  12768  pcz  12770  dvdsprmpweqle  12775  qexpz  12790  4sqlemafi  12833  4sqlem11  12839  ennnfonelemjn  12888  ennnfonelemh  12890  ennnfonelem0  12891  ennnfonelem1  12893  ennnfonelemom  12894  ennnfonelemkh  12898  ennnfonelemhf1o  12899  ennnfonelemex  12900  ennnfonelemrn  12905  ennnfonelemnn0  12908  ctinfomlemom  12913  mulgval  13573  mulgfng  13575  subgmulg  13639  elply2  15322  plyf  15324  elplyd  15328  ply1termlem  15329  plyaddlem1  15334  plymullem1  15335  plymullem  15337  plycoeid3  15344  plycolemc  15345  plycjlemc  15347  plycn  15349  plyrecj  15350  dvply1  15352  sgmppw  15579  0sgmppw  15580  mersenne  15584  lgsval  15596  lgsfvalg  15597  lgscllem  15599  lgsval2lem  15602  lgsneg1  15617  lgsne0  15630  lgsquad3  15676  012of  16130  2o01f  16131  isomninnlem  16171  iswomninnlem  16190  ismkvnnlem  16193  dceqnconst  16201  dcapnconst  16202