Theorem 0zd 9660

Description: Zero is an integer, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
0zd	⊢ (𝜑 → 0 ∈ ℤ)

Proof of Theorem 0zd

Step	Hyp	Ref	Expression
1		0z 9659	. 2 ⊢ 0 ∈ ℤ
2	1	a1i 9	1 ⊢ (𝜑 → 0 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  0cc0 8179  ℤcz 9648

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 8273  ax-addrcl 8276  ax-rnegex 8288

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 8501  df-z 9649

This theorem is used by:  fzctr  10550  fzosubel3  10624  frecfzennn  10876  frechashgf1o  10878  0tonninf  10890  1tonninf  10891  exp3val  10991  exp0  10993  nn0sqdc  11160  bcval  11201  bccmpl  11206  bcval5  11215  bcpasc  11218  bccl  11219  hashcl  11234  hashfiv01gt1  11235  hashfz1  11236  hashen  11237  fihashneq0  11247  omgadd  11256  fihashdom  11257  fiubz  11286  fnfz0hash  11289  ffzo0hash  11291  hashfibc  11297  wrdval  11321  snopiswrd  11328  wrdsymb0  11351  ccatfvalfi  11374  ccatcl  11375  ccatlen  11377  ccatsymb  11384  fzowrddc  11433  swrdval  11434  swrdspsleq  11453  pfxval  11460  fnpfx  11463  pfxclg  11464  pfxnd  11475  pfxwrdsymbg  11476  pfxccatin12lem1  11514  pfxccatin12  11519  swrdccat  11521  fzomaxdiflem  11893  fsumzcl  12185  fisum0diag  12224  fisum0diag2  12230  binomlem  12266  binom1dif  12270  isumnn0nn  12276  expcnvre  12286  explecnv  12288  pwm1geoserap1  12291  geolim  12294  geolim2  12295  geo2sum  12297  geoisum  12300  geoisumr  12301  mertenslemub  12317  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  fprod0diagfz  12411  eftcl  12437  efval  12444  eff  12446  efcvg  12449  efcvgfsum  12450  reefcl  12451  ege2le3  12454  efcj  12456  efaddlem  12457  eftlub  12473  effsumlt  12475  efgt1p2  12478  efgt1p  12479  eflegeo  12484  eirraplem  12560  dvdsmodexp  12578  dvdsmod  12645  3dvds  12647  bitsfzolem  12737  bitsfi  12740  bitsinv1lem  12744  bitsinv1  12745  gcdn0gt0  12771  gcdaddm  12777  gcdmultipled  12786  bezoutlemle  12801  nninfctlemfo  12833  nn0seqcvgd  12835  alginv  12841  algcvg  12842  algcvga  12845  algfx  12846  eucalgval2  12847  eucalgcvga  12852  eucalg  12853  lcmcllem  12861  lcmid  12874  mulgcddvds  12888  divgcdcoprmex  12896  cncongr1  12897  cncongr2  12898  phiprmpw  13020  modprm0  13053  pcpremul  13092  pceu  13094  pcmul  13100  pcqmul  13102  pcge0  13112  pcdvdsb  13119  pcneg  13124  pcgcd1  13127  pc2dvds  13129  pcz  13131  dvdsprmpweqle  13136  qexpz  13151  4sqlemafi  13194  4sqlem11  13200  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemfval0  13284  ballotfilemiex  13293  ennnfonelemjn  13342  ennnfonelemh  13344  ennnfonelem0  13345  ennnfonelem1  13347  ennnfonelemom  13348  ennnfonelemkh  13352  ennnfonelemhf1o  13353  ennnfonelemex  13354  ennnfonelemrn  13359  ennnfonelemnn0  13362  ctinfomlemom  13367  mulgval  13974  mulgfng  13976  subgmulg  14040  elply2  15885  plyf  15887  elplyd  15891  ply1termlem  15892  plyaddlem1  15897  plymullem1  15898  plymullem  15900  plycoeid3  15907  plycolemc  15908  plycjlemc  15910  plycn  15912  plyrecj  15913  dvply1  15915  log2tlbndlog2  16139  log2ublem2  16141  log2ublog2  16143  birthdaylem3  16146  sgmppw  16187  0sgmppw  16188  mersenne  16195  bcmono  16202  lgsval  16221  lgsfvalg  16222  lgscllem  16224  lgsval2lem  16227  lgsneg1  16242  lgsne0  16255  lgsquad3  16301  wksfval  16661  wlkex  16664  iswlkg  16668  depindlem1  16845  012of  17121  2o01f  17122  isomninnlem  17177  iswomninnlem  17197  ismkvnnlem  17200  dceqnconst  17208  dcapnconst  17209