Theorem 0zd 9661

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 9660	. 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 8180   ZZcz 9649

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 8274  ax-addrcl 8277  ax-rnegex 8289

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 4131  df-iota 5337  df-fv 5385  df-ov 6088  df-neg 8502  df-z 9650

This theorem is used by:  fzctr  10551  fzosubel3  10625  frecfzennn  10878  frechashgf1o  10880  0tonninf  10892  1tonninf  10893  exp3val  10993  exp0  10995  nn0sqdc  11162  bcval  11203  bccmpl  11208  bcval5  11217  bcpasc  11220  bccl  11221  hashcl  11236  hashfiv01gt1  11237  hashfz1  11238  hashen  11239  fihashneq0  11249  omgadd  11258  fihashdom  11259  fiubz  11288  fnfz0hash  11291  ffzo0hash  11293  hashfibc  11299  wrdval  11323  snopiswrd  11330  wrdsymb0  11353  ccatfvalfi  11376  ccatcl  11377  ccatlen  11379  ccatsymb  11386  fzowrddc  11435  swrdval  11436  swrdspsleq  11455  pfxval  11462  fnpfx  11465  pfxclg  11466  pfxnd  11477  pfxwrdsymbg  11478  pfxccatin12lem1  11516  pfxccatin12  11521  swrdccat  11523  fzomaxdiflem  11895  fsumzcl  12188  fisum0diag  12227  fisum0diag2  12233  binomlem  12269  binom1dif  12273  isumnn0nn  12279  expcnvre  12289  explecnv  12291  pwm1geoserap1  12294  geolim  12297  geolim2  12298  geo2sum  12300  geoisum  12303  geoisumr  12304  mertenslemub  12320  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  fprod0diagfz  12414  eftcl  12440  efval  12447  eff  12449  efcvg  12452  efcvgfsum  12453  reefcl  12454  ege2le3  12457  efcj  12459  efaddlem  12460  eftlub  12476  effsumlt  12478  efgt1p2  12481  efgt1p  12482  eflegeo  12487  eirraplem  12563  dvdsmodexp  12581  dvdsmod  12648  3dvds  12650  bitsfzolem  12740  bitsfi  12743  bitsinv1lem  12747  bitsinv1  12748  gcdn0gt0  12774  gcdaddm  12780  gcdmultipled  12789  bezoutlemle  12804  nninfctlemfo  12836  nn0seqcvgd  12838  alginv  12844  algcvg  12845  algcvga  12848  algfx  12849  eucalgval2  12850  eucalgcvga  12855  eucalg  12856  lcmcllem  12864  lcmid  12877  mulgcddvds  12891  divgcdcoprmex  12899  cncongr1  12900  cncongr2  12901  phiprmpw  13023  modprm0  13056  pcpremul  13095  pceu  13097  pcmul  13103  pcqmul  13105  pcge0  13115  pcdvdsb  13122  pcneg  13127  pcgcd1  13130  pc2dvds  13132  pcz  13134  dvdsprmpweqle  13139  qexpz  13154  4sqlemafi  13197  4sqlem11  13203  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemfval0  13287  ballotfilemiex  13296  ennnfonelemjn  13345  ennnfonelemh  13347  ennnfonelem0  13348  ennnfonelem1  13350  ennnfonelemom  13351  ennnfonelemkh  13355  ennnfonelemhf1o  13356  ennnfonelemex  13357  ennnfonelemrn  13362  ennnfonelemnn0  13365  ctinfomlemom  13370  mulgval  13978  mulgfng  13980  subgmulg  14044  psrbaglefifi  15147  elply2  15927  plyf  15929  elplyd  15933  ply1termlem  15934  plyaddlem1  15939  plymullem1  15940  plymullem  15942  plycoeid3  15949  plycolemc  15950  plycjlemc  15952  plycn  15954  plyrecj  15955  dvply1  15957  log2tlbndlog2  16181  log2ublem2  16183  log2ublog2  16185  birthdaylem3  16188  sgmppw  16247  0sgmppw  16248  chtublem  16256  mersenne  16258  bcmono  16265  lgsval  16289  lgsfvalg  16290  lgscllem  16292  lgsval2lem  16295  lgsneg1  16310  lgsne0  16323  lgsquad3  16369  wksfval  16729  wlkex  16732  iswlkg  16736  depindlem1  16913  012of  17189  2o01f  17190  isomninnlem  17245  iswomninnlem  17266  ismkvnnlem  17269  dceqnconst  17277  dcapnconst  17278