Theorem 0zd 9552

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

Syntax hints:   -> wi 4   e. wcel 2202   0cc0 8092   ZZcz 9540

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 2213  ax-1re 8186  ax-addrcl 8189  ax-rnegex 8201

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-rab 2520  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031  df-neg 8412  df-z 9541

This theorem is referenced by:  fzctr  10430  fzosubel3  10504  frecfzennn  10751  frechashgf1o  10753  0tonninf  10765  1tonninf  10766  exp3val  10866  exp0  10868  bcval  11074  bccmpl  11079  bcval5  11088  bcpasc  11091  bccl  11092  hashcl  11106  hashfiv01gt1  11107  hashfz1  11108  hashen  11109  fihashneq0  11119  omgadd  11128  fihashdom  11129  fiubz  11156  fnfz0hash  11159  ffzo0hash  11161  wrdval  11182  snopiswrd  11189  wrdsymb0  11212  ccatfvalfi  11235  ccatcl  11236  ccatlen  11238  ccatsymb  11245  fzowrddc  11294  swrdval  11295  swrdspsleq  11314  pfxval  11321  fnpfx  11324  pfxclg  11325  pfxnd  11336  pfxwrdsymbg  11337  pfxccatin12lem1  11375  pfxccatin12  11380  swrdccat  11382  fzomaxdiflem  11752  fsumzcl  12043  fisum0diag  12082  fisum0diag2  12088  binomlem  12124  binom1dif  12128  isumnn0nn  12134  expcnvre  12144  explecnv  12146  pwm1geoserap1  12149  geolim  12152  geolim2  12153  geo2sum  12155  geoisum  12158  geoisumr  12159  mertenslemub  12175  mertenslemi1  12176  mertenslem2  12177  mertensabs  12178  fprod0diagfz  12269  eftcl  12295  efval  12302  eff  12304  efcvg  12307  efcvgfsum  12308  reefcl  12309  ege2le3  12312  efcj  12314  efaddlem  12315  eftlub  12331  effsumlt  12333  efgt1p2  12336  efgt1p  12337  eflegeo  12342  eirraplem  12418  dvdsmodexp  12436  dvdsmod  12503  3dvds  12505  bitsfzolem  12595  bitsfi  12598  bitsinv1lem  12602  bitsinv1  12603  gcdn0gt0  12629  gcdaddm  12635  gcdmultipled  12644  bezoutlemle  12659  nninfctlemfo  12691  nn0seqcvgd  12693  alginv  12699  algcvg  12700  algcvga  12703  algfx  12704  eucalgval2  12705  eucalgcvga  12710  eucalg  12711  lcmcllem  12719  lcmid  12732  mulgcddvds  12746  divgcdcoprmex  12754  cncongr1  12755  cncongr2  12756  phiprmpw  12874  modprm0  12907  pcpremul  12946  pceu  12948  pcmul  12954  pcqmul  12956  pcge0  12966  pcdvdsb  12973  pcneg  12978  pcgcd1  12981  pc2dvds  12983  pcz  12985  dvdsprmpweqle  12990  qexpz  13005  4sqlemafi  13048  4sqlem11  13054  ennnfonelemjn  13103  ennnfonelemh  13105  ennnfonelem0  13106  ennnfonelem1  13108  ennnfonelemom  13109  ennnfonelemkh  13113  ennnfonelemhf1o  13114  ennnfonelemex  13115  ennnfonelemrn  13120  ennnfonelemnn0  13123  ctinfomlemom  13128  mulgval  13789  mulgfng  13791  subgmulg  13855  elply2  15546  plyf  15548  elplyd  15552  ply1termlem  15553  plyaddlem1  15558  plymullem1  15559  plymullem  15561  plycoeid3  15568  plycolemc  15569  plycjlemc  15571  plycn  15573  plyrecj  15574  dvply1  15576  sgmppw  15806  0sgmppw  15807  mersenne  15811  lgsval  15823  lgsfvalg  15824  lgscllem  15826  lgsval2lem  15829  lgsneg1  15844  lgsne0  15857  lgsquad3  15903  wksfval  16263  wlkex  16266  iswlkg  16270  depindlem1  16447  012of  16713  2o01f  16714  isomninnlem  16762  iswomninnlem  16782  ismkvnnlem  16785  dceqnconst  16793  dcapnconst  16794