Theorem 0zd 9635

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

Syntax hints:   -> wi 4   e. wcel 2209   0cc0 8169   ZZcz 9623

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1re 8263  ax-addrcl 8266  ax-rnegex 8278

This theorem depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-rab 2537  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380  df-ov 6078  df-neg 8490  df-z 9624

This theorem is referenced by:  fzctr  10518  fzosubel3  10592  frecfzennn  10841  frechashgf1o  10843  0tonninf  10855  1tonninf  10856  exp3val  10956  exp0  10958  bcval  11165  bccmpl  11170  bcval5  11179  bcpasc  11182  bccl  11183  hashcl  11198  hashfiv01gt1  11199  hashfz1  11200  hashen  11201  fihashneq0  11211  omgadd  11220  fihashdom  11221  fiubz  11250  fnfz0hash  11253  ffzo0hash  11255  hashfibc  11261  wrdval  11285  snopiswrd  11292  wrdsymb0  11315  ccatfvalfi  11338  ccatcl  11339  ccatlen  11341  ccatsymb  11348  fzowrddc  11397  swrdval  11398  swrdspsleq  11417  pfxval  11424  fnpfx  11427  pfxclg  11428  pfxnd  11439  pfxwrdsymbg  11440  pfxccatin12lem1  11478  pfxccatin12  11483  swrdccat  11485  fzomaxdiflem  11856  fsumzcl  12147  fisum0diag  12186  fisum0diag2  12192  binomlem  12228  binom1dif  12232  isumnn0nn  12238  expcnvre  12248  explecnv  12250  pwm1geoserap1  12253  geolim  12256  geolim2  12257  geo2sum  12259  geoisum  12262  geoisumr  12263  mertenslemub  12279  mertenslemi1  12280  mertenslem2  12281  mertensabs  12282  fprod0diagfz  12373  eftcl  12399  efval  12406  eff  12408  efcvg  12411  efcvgfsum  12412  reefcl  12413  ege2le3  12416  efcj  12418  efaddlem  12419  eftlub  12435  effsumlt  12437  efgt1p2  12440  efgt1p  12441  eflegeo  12446  eirraplem  12522  dvdsmodexp  12540  dvdsmod  12607  3dvds  12609  bitsfzolem  12699  bitsfi  12702  bitsinv1lem  12706  bitsinv1  12707  gcdn0gt0  12733  gcdaddm  12739  gcdmultipled  12748  bezoutlemle  12763  nninfctlemfo  12795  nn0seqcvgd  12797  alginv  12803  algcvg  12804  algcvga  12807  algfx  12808  eucalgval2  12809  eucalgcvga  12814  eucalg  12815  lcmcllem  12823  lcmid  12836  mulgcddvds  12850  divgcdcoprmex  12858  cncongr1  12859  cncongr2  12860  phiprmpw  12978  modprm0  13011  pcpremul  13050  pceu  13052  pcmul  13058  pcqmul  13060  pcge0  13070  pcdvdsb  13077  pcneg  13082  pcgcd1  13085  pc2dvds  13087  pcz  13089  dvdsprmpweqle  13094  qexpz  13109  4sqlemafi  13152  4sqlem11  13158  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemfval0  13213  ballotfilemiex  13222  ennnfonelemjn  13271  ennnfonelemh  13273  ennnfonelem0  13274  ennnfonelem1  13276  ennnfonelemom  13277  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ennnfonelemex  13283  ennnfonelemrn  13288  ennnfonelemnn0  13291  ctinfomlemom  13296  mulgval  13902  mulgfng  13904  subgmulg  13968  elply2  15759  plyf  15761  elplyd  15765  ply1termlem  15766  plyaddlem1  15771  plymullem1  15772  plymullem  15774  plycoeid3  15781  plycolemc  15782  plycjlemc  15784  plycn  15786  plyrecj  15787  dvply1  15789  sgmppw  16020  0sgmppw  16021  mersenne  16025  lgsval  16037  lgsfvalg  16038  lgscllem  16040  lgsval2lem  16043  lgsneg1  16058  lgsne0  16071  lgsquad3  16117  wksfval  16477  wlkex  16480  iswlkg  16484  depindlem1  16661  012of  16937  2o01f  16938  isomninnlem  16984  iswomninnlem  17004  ismkvnnlem  17007  dceqnconst  17015  dcapnconst  17016