Theorem 0zd 9656

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

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

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 8500  df-z 9645

This theorem is used by:  fzctr  10540  fzosubel3  10614  frecfzennn  10863  frechashgf1o  10865  0tonninf  10877  1tonninf  10878  exp3val  10978  exp0  10980  bcval  11187  bccmpl  11192  bcval5  11201  bcpasc  11204  bccl  11205  hashcl  11220  hashfiv01gt1  11221  hashfz1  11222  hashen  11223  fihashneq0  11233  omgadd  11242  fihashdom  11243  fiubz  11272  fnfz0hash  11275  ffzo0hash  11277  hashfibc  11283  wrdval  11307  snopiswrd  11314  wrdsymb0  11337  ccatfvalfi  11360  ccatcl  11361  ccatlen  11363  ccatsymb  11370  fzowrddc  11419  swrdval  11420  swrdspsleq  11439  pfxval  11446  fnpfx  11449  pfxclg  11450  pfxnd  11461  pfxwrdsymbg  11462  pfxccatin12lem1  11500  pfxccatin12  11505  swrdccat  11507  fzomaxdiflem  11878  fsumzcl  12169  fisum0diag  12208  fisum0diag2  12214  binomlem  12250  binom1dif  12254  isumnn0nn  12260  expcnvre  12270  explecnv  12272  pwm1geoserap1  12275  geolim  12278  geolim2  12279  geo2sum  12281  geoisum  12284  geoisumr  12285  mertenslemub  12301  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  fprod0diagfz  12395  eftcl  12421  efval  12428  eff  12430  efcvg  12433  efcvgfsum  12434  reefcl  12435  ege2le3  12438  efcj  12440  efaddlem  12441  eftlub  12457  effsumlt  12459  efgt1p2  12462  efgt1p  12463  eflegeo  12468  eirraplem  12544  dvdsmodexp  12562  dvdsmod  12629  3dvds  12631  bitsfzolem  12721  bitsfi  12724  bitsinv1lem  12728  bitsinv1  12729  gcdn0gt0  12755  gcdaddm  12761  gcdmultipled  12770  bezoutlemle  12785  nninfctlemfo  12817  nn0seqcvgd  12819  alginv  12825  algcvg  12826  algcvga  12829  algfx  12830  eucalgval2  12831  eucalgcvga  12836  eucalg  12837  lcmcllem  12845  lcmid  12858  mulgcddvds  12872  divgcdcoprmex  12880  cncongr1  12881  cncongr2  12882  phiprmpw  13000  modprm0  13033  pcpremul  13072  pceu  13074  pcmul  13080  pcqmul  13082  pcge0  13092  pcdvdsb  13099  pcneg  13104  pcgcd1  13107  pc2dvds  13109  pcz  13111  dvdsprmpweqle  13116  qexpz  13131  4sqlemafi  13174  4sqlem11  13180  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemfval0  13235  ballotfilemiex  13244  ennnfonelemjn  13293  ennnfonelemh  13295  ennnfonelem0  13296  ennnfonelem1  13298  ennnfonelemom  13299  ennnfonelemkh  13303  ennnfonelemhf1o  13304  ennnfonelemex  13305  ennnfonelemrn  13310  ennnfonelemnn0  13313  ctinfomlemom  13318  mulgval  13925  mulgfng  13927  subgmulg  13991  elply2  15836  plyf  15838  elplyd  15842  ply1termlem  15843  plyaddlem1  15848  plymullem1  15849  plymullem  15851  plycoeid3  15858  plycolemc  15859  plycjlemc  15861  plycn  15863  plyrecj  15864  dvply1  15866  log2tlbndlog2  16082  log2ublem2  16084  log2ublog2  16086  birthdaylem3  16089  sgmppw  16106  0sgmppw  16107  mersenne  16111  lgsval  16123  lgsfvalg  16124  lgscllem  16126  lgsval2lem  16129  lgsneg1  16144  lgsne0  16157  lgsquad3  16203  wksfval  16563  wlkex  16566  iswlkg  16570  depindlem1  16747  012of  17023  2o01f  17024  isomninnlem  17079  iswomninnlem  17099  ismkvnnlem  17102  dceqnconst  17110  dcapnconst  17111