Theorem 0zd 9606

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 9605	. 2 ⊢ 0 ∈ ℤ
2	1	a1i 9	1 ⊢ (𝜑 → 0 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2205  0cc0 8143  ℤcz 9594

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 2216  ax-1re 8237  ax-addrcl 8240  ax-rnegex 8252

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-rab 2531  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061  df-neg 8463  df-z 9595

This theorem is referenced by:  fzctr  10489  fzosubel3  10563  frecfzennn  10812  frechashgf1o  10814  0tonninf  10826  1tonninf  10827  exp3val  10927  exp0  10929  bcval  11136  bccmpl  11141  bcval5  11150  bcpasc  11153  bccl  11154  hashcl  11169  hashfiv01gt1  11170  hashfz1  11171  hashen  11172  fihashneq0  11182  omgadd  11191  fihashdom  11192  fiubz  11221  fnfz0hash  11224  ffzo0hash  11226  hashfibc  11232  wrdval  11252  snopiswrd  11259  wrdsymb0  11282  ccatfvalfi  11305  ccatcl  11306  ccatlen  11308  ccatsymb  11315  fzowrddc  11364  swrdval  11365  swrdspsleq  11384  pfxval  11391  fnpfx  11394  pfxclg  11395  pfxnd  11406  pfxwrdsymbg  11407  pfxccatin12lem1  11445  pfxccatin12  11450  swrdccat  11452  fzomaxdiflem  11822  fsumzcl  12113  fisum0diag  12152  fisum0diag2  12158  binomlem  12194  binom1dif  12198  isumnn0nn  12204  expcnvre  12214  explecnv  12216  pwm1geoserap1  12219  geolim  12222  geolim2  12223  geo2sum  12225  geoisum  12228  geoisumr  12229  mertenslemub  12245  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  fprod0diagfz  12339  eftcl  12365  efval  12372  eff  12374  efcvg  12377  efcvgfsum  12378  reefcl  12379  ege2le3  12382  efcj  12384  efaddlem  12385  eftlub  12401  effsumlt  12403  efgt1p2  12406  efgt1p  12407  eflegeo  12412  eirraplem  12488  dvdsmodexp  12506  dvdsmod  12573  3dvds  12575  bitsfzolem  12665  bitsfi  12668  bitsinv1lem  12672  bitsinv1  12673  gcdn0gt0  12699  gcdaddm  12705  gcdmultipled  12714  bezoutlemle  12729  nninfctlemfo  12761  nn0seqcvgd  12763  alginv  12769  algcvg  12770  algcvga  12773  algfx  12774  eucalgval2  12775  eucalgcvga  12780  eucalg  12781  lcmcllem  12789  lcmid  12802  mulgcddvds  12816  divgcdcoprmex  12824  cncongr1  12825  cncongr2  12826  phiprmpw  12944  modprm0  12977  pcpremul  13016  pceu  13018  pcmul  13024  pcqmul  13026  pcge0  13036  pcdvdsb  13043  pcneg  13048  pcgcd1  13051  pc2dvds  13053  pcz  13055  dvdsprmpweqle  13060  qexpz  13075  4sqlemafi  13118  4sqlem11  13124  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemfval0  13179  ballotfilemiex  13188  ennnfonelemjn  13237  ennnfonelemh  13239  ennnfonelem0  13240  ennnfonelem1  13242  ennnfonelemom  13243  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ennnfonelemex  13249  ennnfonelemrn  13254  ennnfonelemnn0  13257  ctinfomlemom  13262  mulgval  13875  mulgfng  13877  subgmulg  13941  elply2  15726  plyf  15728  elplyd  15732  ply1termlem  15733  plyaddlem1  15738  plymullem1  15739  plymullem  15741  plycoeid3  15748  plycolemc  15749  plycjlemc  15751  plycn  15753  plyrecj  15754  dvply1  15756  sgmppw  15986  0sgmppw  15987  mersenne  15991  lgsval  16003  lgsfvalg  16004  lgscllem  16006  lgsval2lem  16009  lgsneg1  16024  lgsne0  16037  lgsquad3  16083  wksfval  16443  wlkex  16446  iswlkg  16450  depindlem1  16627  012of  16893  2o01f  16894  isomninnlem  16940  iswomninnlem  16960  ismkvnnlem  16963  dceqnconst  16972  dcapnconst  16973