Theorem 0zd 9264

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

Syntax hints:   -> wi 4   e. wcel 2148   0cc0 7810   ZZcz 9252

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1re 7904  ax-addrcl 7907  ax-rnegex 7919

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877  df-neg 8130  df-z 9253

This theorem is referenced by:  fzctr  10132  fzosubel3  10195  frecfzennn  10425  frechashgf1o  10427  0tonninf  10438  1tonninf  10439  exp3val  10521  exp0  10523  bcval  10728  bccmpl  10733  bcval5  10742  bcpasc  10745  bccl  10746  hashcl  10760  hashfiv01gt1  10761  hashfz1  10762  hashen  10763  fihashneq0  10773  omgadd  10781  fihashdom  10782  fiubz  10808  fnfz0hash  10811  ffzo0hash  10813  fzomaxdiflem  11120  fsumzcl  11409  fisum0diag  11448  fisum0diag2  11454  binomlem  11490  binom1dif  11494  isumnn0nn  11500  expcnvre  11510  explecnv  11512  pwm1geoserap1  11515  geolim  11518  geolim2  11519  geo2sum  11521  geoisum  11524  geoisumr  11525  mertenslemub  11541  mertenslemi1  11542  mertenslem2  11543  mertensabs  11544  fprod0diagfz  11635  eftcl  11661  efval  11668  eff  11670  efcvg  11673  efcvgfsum  11674  reefcl  11675  ege2le3  11678  efcj  11680  efaddlem  11681  eftlub  11697  effsumlt  11699  efgt1p2  11702  efgt1p  11703  eflegeo  11708  eirraplem  11783  dvdsmodexp  11801  dvdsmod  11867  gcdn0gt0  11978  gcdaddm  11984  gcdmultipled  11993  bezoutlemle  12008  nn0seqcvgd  12040  alginv  12046  algcvg  12047  algcvga  12050  algfx  12051  eucalgval2  12052  eucalgcvga  12057  eucalg  12058  lcmcllem  12066  lcmid  12079  mulgcddvds  12093  divgcdcoprmex  12101  cncongr1  12102  cncongr2  12103  phiprmpw  12221  modprm0  12253  pcpremul  12292  pceu  12294  pcmul  12300  pcqmul  12302  pcge0  12311  pcdvdsb  12318  pcneg  12323  pcgcd1  12326  pc2dvds  12328  pcz  12330  dvdsprmpweqle  12335  qexpz  12349  ennnfonelemjn  12402  ennnfonelemh  12404  ennnfonelem0  12405  ennnfonelem1  12407  ennnfonelemom  12408  ennnfonelemkh  12412  ennnfonelemhf1o  12413  ennnfonelemex  12414  ennnfonelemrn  12419  ennnfonelemnn0  12422  ctinfomlemom  12427  mulgval  12985  mulgfng  12986  subgmulg  13046  lgsval  14375  lgsfvalg  14376  lgscllem  14378  lgsval2lem  14381  lgsneg1  14396  lgsne0  14409  012of  14715  2o01f  14716  isomninnlem  14748  iswomninnlem  14767  ismkvnnlem  14770  dceqnconst  14777  dcapnconst  14778