Theorem 0zd 9469

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

Syntax hints:   -> wi 4   e. wcel 2200   0cc0 8010   ZZcz 9457

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8104  ax-addrcl 8107  ax-rnegex 8119

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010  df-neg 8331  df-z 9458

This theorem is referenced by:  fzctr  10341  fzosubel3  10414  frecfzennn  10660  frechashgf1o  10662  0tonninf  10674  1tonninf  10675  exp3val  10775  exp0  10777  bcval  10983  bccmpl  10988  bcval5  10997  bcpasc  11000  bccl  11001  hashcl  11015  hashfiv01gt1  11016  hashfz1  11017  hashen  11018  fihashneq0  11028  omgadd  11036  fihashdom  11037  fiubz  11064  fnfz0hash  11067  ffzo0hash  11069  wrdval  11087  snopiswrd  11094  wrdsymb0  11117  ccatfvalfi  11140  ccatcl  11141  ccatlen  11143  ccatsymb  11150  fzowrddc  11195  swrdval  11196  swrdspsleq  11215  pfxval  11222  fnpfx  11225  pfxclg  11226  pfxnd  11237  pfxwrdsymbg  11238  pfxccatin12lem1  11276  pfxccatin12  11281  swrdccat  11283  fzomaxdiflem  11639  fsumzcl  11929  fisum0diag  11968  fisum0diag2  11974  binomlem  12010  binom1dif  12014  isumnn0nn  12020  expcnvre  12030  explecnv  12032  pwm1geoserap1  12035  geolim  12038  geolim2  12039  geo2sum  12041  geoisum  12044  geoisumr  12045  mertenslemub  12061  mertenslemi1  12062  mertenslem2  12063  mertensabs  12064  fprod0diagfz  12155  eftcl  12181  efval  12188  eff  12190  efcvg  12193  efcvgfsum  12194  reefcl  12195  ege2le3  12198  efcj  12200  efaddlem  12201  eftlub  12217  effsumlt  12219  efgt1p2  12222  efgt1p  12223  eflegeo  12228  eirraplem  12304  dvdsmodexp  12322  dvdsmod  12389  3dvds  12391  bitsfzolem  12481  bitsfi  12484  bitsinv1lem  12488  bitsinv1  12489  gcdn0gt0  12515  gcdaddm  12521  gcdmultipled  12530  bezoutlemle  12545  nninfctlemfo  12577  nn0seqcvgd  12579  alginv  12585  algcvg  12586  algcvga  12589  algfx  12590  eucalgval2  12591  eucalgcvga  12596  eucalg  12597  lcmcllem  12605  lcmid  12618  mulgcddvds  12632  divgcdcoprmex  12640  cncongr1  12641  cncongr2  12642  phiprmpw  12760  modprm0  12793  pcpremul  12832  pceu  12834  pcmul  12840  pcqmul  12842  pcge0  12852  pcdvdsb  12859  pcneg  12864  pcgcd1  12867  pc2dvds  12869  pcz  12871  dvdsprmpweqle  12876  qexpz  12891  4sqlemafi  12934  4sqlem11  12940  ennnfonelemjn  12989  ennnfonelemh  12991  ennnfonelem0  12992  ennnfonelem1  12994  ennnfonelemom  12995  ennnfonelemkh  12999  ennnfonelemhf1o  13000  ennnfonelemex  13001  ennnfonelemrn  13006  ennnfonelemnn0  13009  ctinfomlemom  13014  mulgval  13675  mulgfng  13677  subgmulg  13741  elply2  15425  plyf  15427  elplyd  15431  ply1termlem  15432  plyaddlem1  15437  plymullem1  15438  plymullem  15440  plycoeid3  15447  plycolemc  15448  plycjlemc  15450  plycn  15452  plyrecj  15453  dvply1  15455  sgmppw  15682  0sgmppw  15683  mersenne  15687  lgsval  15699  lgsfvalg  15700  lgscllem  15702  lgsval2lem  15705  lgsneg1  15720  lgsne0  15733  lgsquad3  15779  wksfval  16068  wlkex  16071  iswlkg  16075  012of  16444  2o01f  16445  isomninnlem  16486  iswomninnlem  16505  ismkvnnlem  16508  dceqnconst  16516  dcapnconst  16517