Theorem 0zd 9589

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

Syntax hints:   -> wi 4   e. wcel 2203   0cc0 8127   ZZcz 9577

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-1re 8221  ax-addrcl 8224  ax-rnegex 8236

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-rab 2529  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360  df-ov 6053  df-neg 8447  df-z 9578

This theorem is referenced by:  fzctr  10467  fzosubel3  10541  frecfzennn  10788  frechashgf1o  10790  0tonninf  10802  1tonninf  10803  exp3val  10903  exp0  10905  bcval  11111  bccmpl  11116  bcval5  11125  bcpasc  11128  bccl  11129  hashcl  11144  hashfiv01gt1  11145  hashfz1  11146  hashen  11147  fihashneq0  11157  omgadd  11166  fihashdom  11167  fiubz  11196  fnfz0hash  11199  ffzo0hash  11201  hashfibc  11207  wrdval  11227  snopiswrd  11234  wrdsymb0  11257  ccatfvalfi  11280  ccatcl  11281  ccatlen  11283  ccatsymb  11290  fzowrddc  11339  swrdval  11340  swrdspsleq  11359  pfxval  11366  fnpfx  11369  pfxclg  11370  pfxnd  11381  pfxwrdsymbg  11382  pfxccatin12lem1  11420  pfxccatin12  11425  swrdccat  11427  fzomaxdiflem  11797  fsumzcl  12088  fisum0diag  12127  fisum0diag2  12133  binomlem  12169  binom1dif  12173  isumnn0nn  12179  expcnvre  12189  explecnv  12191  pwm1geoserap1  12194  geolim  12197  geolim2  12198  geo2sum  12200  geoisum  12203  geoisumr  12204  mertenslemub  12220  mertenslemi1  12221  mertenslem2  12222  mertensabs  12223  fprod0diagfz  12314  eftcl  12340  efval  12347  eff  12349  efcvg  12352  efcvgfsum  12353  reefcl  12354  ege2le3  12357  efcj  12359  efaddlem  12360  eftlub  12376  effsumlt  12378  efgt1p2  12381  efgt1p  12382  eflegeo  12387  eirraplem  12463  dvdsmodexp  12481  dvdsmod  12548  3dvds  12550  bitsfzolem  12640  bitsfi  12643  bitsinv1lem  12647  bitsinv1  12648  gcdn0gt0  12674  gcdaddm  12680  gcdmultipled  12689  bezoutlemle  12704  nninfctlemfo  12736  nn0seqcvgd  12738  alginv  12744  algcvg  12745  algcvga  12748  algfx  12749  eucalgval2  12750  eucalgcvga  12755  eucalg  12756  lcmcllem  12764  lcmid  12777  mulgcddvds  12791  divgcdcoprmex  12799  cncongr1  12800  cncongr2  12801  phiprmpw  12919  modprm0  12952  pcpremul  12991  pceu  12993  pcmul  12999  pcqmul  13001  pcge0  13011  pcdvdsb  13018  pcneg  13023  pcgcd1  13026  pc2dvds  13028  pcz  13030  dvdsprmpweqle  13035  qexpz  13050  4sqlemafi  13093  4sqlem11  13099  ennnfonelemjn  13153  ennnfonelemh  13155  ennnfonelem0  13156  ennnfonelem1  13158  ennnfonelemom  13159  ennnfonelemkh  13163  ennnfonelemhf1o  13164  ennnfonelemex  13165  ennnfonelemrn  13170  ennnfonelemnn0  13173  ctinfomlemom  13178  mulgval  13839  mulgfng  13841  subgmulg  13905  elply2  15600  plyf  15602  elplyd  15606  ply1termlem  15607  plyaddlem1  15612  plymullem1  15613  plymullem  15615  plycoeid3  15622  plycolemc  15623  plycjlemc  15625  plycn  15627  plyrecj  15628  dvply1  15630  sgmppw  15860  0sgmppw  15861  mersenne  15865  lgsval  15877  lgsfvalg  15878  lgscllem  15880  lgsval2lem  15883  lgsneg1  15898  lgsne0  15911  lgsquad3  15957  wksfval  16317  wlkex  16320  iswlkg  16324  depindlem1  16501  012of  16767  2o01f  16768  isomninnlem  16814  iswomninnlem  16834  ismkvnnlem  16837  dceqnconst  16846  dcapnconst  16847