Theorem 0zd 9329

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

Syntax hints:   -> wi 4   e. wcel 2164   0cc0 7872   ZZcz 9317

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-1re 7966  ax-addrcl 7969  ax-rnegex 7981

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-rab 2481  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262  df-ov 5921  df-neg 8193  df-z 9318

This theorem is referenced by:  fzctr  10199  fzosubel3  10263  frecfzennn  10497  frechashgf1o  10499  0tonninf  10511  1tonninf  10512  exp3val  10612  exp0  10614  bcval  10820  bccmpl  10825  bcval5  10834  bcpasc  10837  bccl  10838  hashcl  10852  hashfiv01gt1  10853  hashfz1  10854  hashen  10855  fihashneq0  10865  omgadd  10873  fihashdom  10874  fiubz  10900  fnfz0hash  10903  ffzo0hash  10905  wrdval  10917  snopiswrd  10924  wrdsymb0  10946  fzomaxdiflem  11256  fsumzcl  11545  fisum0diag  11584  fisum0diag2  11590  binomlem  11626  binom1dif  11630  isumnn0nn  11636  expcnvre  11646  explecnv  11648  pwm1geoserap1  11651  geolim  11654  geolim2  11655  geo2sum  11657  geoisum  11660  geoisumr  11661  mertenslemub  11677  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  fprod0diagfz  11771  eftcl  11797  efval  11804  eff  11806  efcvg  11809  efcvgfsum  11810  reefcl  11811  ege2le3  11814  efcj  11816  efaddlem  11817  eftlub  11833  effsumlt  11835  efgt1p2  11838  efgt1p  11839  eflegeo  11844  eirraplem  11920  dvdsmodexp  11938  dvdsmod  12004  gcdn0gt0  12115  gcdaddm  12121  gcdmultipled  12130  bezoutlemle  12145  nninfctlemfo  12177  nn0seqcvgd  12179  alginv  12185  algcvg  12186  algcvga  12189  algfx  12190  eucalgval2  12191  eucalgcvga  12196  eucalg  12197  lcmcllem  12205  lcmid  12218  mulgcddvds  12232  divgcdcoprmex  12240  cncongr1  12241  cncongr2  12242  phiprmpw  12360  modprm0  12392  pcpremul  12431  pceu  12433  pcmul  12439  pcqmul  12441  pcge0  12451  pcdvdsb  12458  pcneg  12463  pcgcd1  12466  pc2dvds  12468  pcz  12470  dvdsprmpweqle  12475  qexpz  12490  4sqlemafi  12533  4sqlem11  12539  ennnfonelemjn  12559  ennnfonelemh  12561  ennnfonelem0  12562  ennnfonelem1  12564  ennnfonelemom  12565  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ennnfonelemex  12571  ennnfonelemrn  12576  ennnfonelemnn0  12579  ctinfomlemom  12584  mulgval  13192  mulgfng  13194  subgmulg  13258  elply2  14881  plyf  14883  elplyd  14887  ply1termlem  14888  plyaddlem1  14893  plymullem1  14894  plymullem  14896  lgsval  15120  lgsfvalg  15121  lgscllem  15123  lgsval2lem  15126  lgsneg1  15141  lgsne0  15154  012of  15486  2o01f  15487  isomninnlem  15520  iswomninnlem  15539  ismkvnnlem  15542  dceqnconst  15550  dcapnconst  15551