Theorem 0zd 9535

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

Syntax hints:   → wi 4   ∈ wcel 2202  0cc0 8075  ℤcz 9523

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 8169  ax-addrcl 8172  ax-rnegex 8184

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 8395  df-z 9524

This theorem is referenced by:  fzctr  10413  fzosubel3  10487  frecfzennn  10734  frechashgf1o  10736  0tonninf  10748  1tonninf  10749  exp3val  10849  exp0  10851  bcval  11057  bccmpl  11062  bcval5  11071  bcpasc  11074  bccl  11075  hashcl  11089  hashfiv01gt1  11090  hashfz1  11091  hashen  11092  fihashneq0  11102  omgadd  11111  fihashdom  11112  fiubz  11139  fnfz0hash  11142  ffzo0hash  11144  wrdval  11165  snopiswrd  11172  wrdsymb0  11195  ccatfvalfi  11218  ccatcl  11219  ccatlen  11221  ccatsymb  11228  fzowrddc  11277  swrdval  11278  swrdspsleq  11297  pfxval  11304  fnpfx  11307  pfxclg  11308  pfxnd  11319  pfxwrdsymbg  11320  pfxccatin12lem1  11358  pfxccatin12  11363  swrdccat  11365  fzomaxdiflem  11735  fsumzcl  12026  fisum0diag  12065  fisum0diag2  12071  binomlem  12107  binom1dif  12111  isumnn0nn  12117  expcnvre  12127  explecnv  12129  pwm1geoserap1  12132  geolim  12135  geolim2  12136  geo2sum  12138  geoisum  12141  geoisumr  12142  mertenslemub  12158  mertenslemi1  12159  mertenslem2  12160  mertensabs  12161  fprod0diagfz  12252  eftcl  12278  efval  12285  eff  12287  efcvg  12290  efcvgfsum  12291  reefcl  12292  ege2le3  12295  efcj  12297  efaddlem  12298  eftlub  12314  effsumlt  12316  efgt1p2  12319  efgt1p  12320  eflegeo  12325  eirraplem  12401  dvdsmodexp  12419  dvdsmod  12486  3dvds  12488  bitsfzolem  12578  bitsfi  12581  bitsinv1lem  12585  bitsinv1  12586  gcdn0gt0  12612  gcdaddm  12618  gcdmultipled  12627  bezoutlemle  12642  nninfctlemfo  12674  nn0seqcvgd  12676  alginv  12682  algcvg  12683  algcvga  12686  algfx  12687  eucalgval2  12688  eucalgcvga  12693  eucalg  12694  lcmcllem  12702  lcmid  12715  mulgcddvds  12729  divgcdcoprmex  12737  cncongr1  12738  cncongr2  12739  phiprmpw  12857  modprm0  12890  pcpremul  12929  pceu  12931  pcmul  12937  pcqmul  12939  pcge0  12949  pcdvdsb  12956  pcneg  12961  pcgcd1  12964  pc2dvds  12966  pcz  12968  dvdsprmpweqle  12973  qexpz  12988  4sqlemafi  13031  4sqlem11  13037  ennnfonelemjn  13086  ennnfonelemh  13088  ennnfonelem0  13089  ennnfonelem1  13091  ennnfonelemom  13092  ennnfonelemkh  13096  ennnfonelemhf1o  13097  ennnfonelemex  13098  ennnfonelemrn  13103  ennnfonelemnn0  13106  ctinfomlemom  13111  mulgval  13772  mulgfng  13774  subgmulg  13838  elply2  15529  plyf  15531  elplyd  15535  ply1termlem  15536  plyaddlem1  15541  plymullem1  15542  plymullem  15544  plycoeid3  15551  plycolemc  15552  plycjlemc  15554  plycn  15556  plyrecj  15557  dvply1  15559  sgmppw  15789  0sgmppw  15790  mersenne  15794  lgsval  15806  lgsfvalg  15807  lgscllem  15809  lgsval2lem  15812  lgsneg1  15827  lgsne0  15840  lgsquad3  15886  wksfval  16246  wlkex  16249  iswlkg  16253  depindlem1  16430  012of  16696  2o01f  16697  isomninnlem  16745  iswomninnlem  16765  ismkvnnlem  16768  dceqnconst  16776  dcapnconst  16777