Theorem 0zd 9665

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   0cc0 8185   ZZcz 9653

This proof depends on 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 8279  ax-addrcl 8282  ax-rnegex 8294

This proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388  df-ov 6091  df-neg 8507  df-z 9654

This theorem is used by:  fzctr  10556  fzosubel3  10630  frecfzennn  10883  frechashgf1o  10885  0tonninf  10897  1tonninf  10898  exp3val  10998  exp0  11000  nn0sqdc  11167  bcval  11208  bccmpl  11213  bcval5  11222  bcpasc  11225  bccl  11226  hashcl  11241  hashfiv01gt1  11242  hashfz1  11243  hashen  11244  fihashneq0  11254  omgadd  11263  fihashdom  11264  fiubz  11293  fnfz0hash  11296  ffzo0hash  11298  hashfibc  11304  wrdval  11328  snopiswrd  11335  wrdsymb0  11358  ccatfvalfi  11381  ccatcl  11382  ccatlen  11384  ccatsymb  11391  fzowrddc  11440  swrdval  11441  swrdspsleq  11460  pfxval  11467  fnpfx  11470  pfxclg  11471  pfxnd  11482  pfxwrdsymbg  11483  pfxccatin12lem1  11521  pfxccatin12  11526  swrdccat  11528  fzomaxdiflem  11900  fsumzcl  12193  fisum0diag  12232  fisum0diag2  12238  binomlem  12274  binom1dif  12278  isumnn0nn  12284  expcnvre  12294  explecnv  12296  pwm1geoserap1  12299  geolim  12302  geolim2  12303  geo2sum  12305  geoisum  12308  geoisumr  12309  mertenslemub  12325  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  fprod0diagfz  12419  eftcl  12445  efval  12452  eff  12454  efcvg  12457  efcvgfsum  12458  reefcl  12459  ege2le3  12462  efcj  12464  efaddlem  12465  eftlub  12481  effsumlt  12483  efgt1p2  12486  efgt1p  12487  eflegeo  12492  eirraplem  12568  dvdsmodexp  12586  dvdsmod  12653  3dvds  12655  bitsfzolem  12745  bitsfi  12748  bitsinv1lem  12752  bitsinv1  12753  gcdn0gt0  12779  gcdaddm  12785  gcdmultipled  12794  bezoutlemle  12809  nninfctlemfo  12841  nn0seqcvgd  12843  alginv  12849  algcvg  12850  algcvga  12853  algfx  12854  eucalgval2  12855  eucalgcvga  12860  eucalg  12861  lcmcllem  12869  lcmid  12882  mulgcddvds  12896  divgcdcoprmex  12904  cncongr1  12905  cncongr2  12906  phiprmpw  13028  modprm0  13061  pcpremul  13100  pceu  13102  pcmul  13108  pcqmul  13110  pcge0  13120  pcdvdsb  13127  pcneg  13132  pcgcd1  13135  pc2dvds  13137  pcz  13139  dvdsprmpweqle  13144  qexpz  13159  4sqlemafi  13202  4sqlem11  13208  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemfval0  13292  ballotfilemiex  13301  ennnfonelemjn  13350  ennnfonelemh  13352  ennnfonelem0  13353  ennnfonelem1  13355  ennnfonelemom  13356  ennnfonelemkh  13360  ennnfonelemhf1o  13361  ennnfonelemex  13362  ennnfonelemrn  13367  ennnfonelemnn0  13370  ctinfomlemom  13375  mulgval  13983  mulgfng  13985  subgmulg  14049  psrbaglefifi  15175  elply2  15978  plyf  15980  elplyd  15984  ply1termlem  15985  plyaddlem1  15990  plymullem1  15991  plymullem  15993  plycoeid3  16000  plycolemc  16001  plycjlemc  16003  plycn  16005  plyrecj  16006  dvply1  16008  log2tlbndlog2  16237  log2ublem2  16239  log2ublog2  16241  birthdaylem3  16244  sgmppw  16303  0sgmppw  16304  chtublem  16312  mersenne  16314  bcmono  16321  lgsval  16345  lgsfvalg  16346  lgscllem  16348  lgsval2lem  16351  lgsneg1  16366  lgsne0  16379  lgsquad3  16425  wksfval  16785  wlkex  16788  iswlkg  16792  depindlem1  16969  012of  17245  2o01f  17246  isomninnlem  17302  iswomninnlem  17323  ismkvnnlem  17326  dceqnconst  17334  dcapnconst  17335