Theorem 0zd 9491

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

Syntax hints:   → wi 4   ∈ wcel 2202  0cc0 8032  ℤcz 9479

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1re 8126  ax-addrcl 8129  ax-rnegex 8141

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021  df-neg 8353  df-z 9480

This theorem is referenced by:  fzctr  10368  fzosubel3  10442  frecfzennn  10689  frechashgf1o  10691  0tonninf  10703  1tonninf  10704  exp3val  10804  exp0  10806  bcval  11012  bccmpl  11017  bcval5  11026  bcpasc  11029  bccl  11030  hashcl  11044  hashfiv01gt1  11045  hashfz1  11046  hashen  11047  fihashneq0  11057  omgadd  11066  fihashdom  11067  fiubz  11094  fnfz0hash  11097  ffzo0hash  11099  wrdval  11117  snopiswrd  11124  wrdsymb0  11147  ccatfvalfi  11170  ccatcl  11171  ccatlen  11173  ccatsymb  11180  fzowrddc  11229  swrdval  11230  swrdspsleq  11249  pfxval  11256  fnpfx  11259  pfxclg  11260  pfxnd  11271  pfxwrdsymbg  11272  pfxccatin12lem1  11310  pfxccatin12  11315  swrdccat  11317  fzomaxdiflem  11674  fsumzcl  11965  fisum0diag  12004  fisum0diag2  12010  binomlem  12046  binom1dif  12050  isumnn0nn  12056  expcnvre  12066  explecnv  12068  pwm1geoserap1  12071  geolim  12074  geolim2  12075  geo2sum  12077  geoisum  12080  geoisumr  12081  mertenslemub  12097  mertenslemi1  12098  mertenslem2  12099  mertensabs  12100  fprod0diagfz  12191  eftcl  12217  efval  12224  eff  12226  efcvg  12229  efcvgfsum  12230  reefcl  12231  ege2le3  12234  efcj  12236  efaddlem  12237  eftlub  12253  effsumlt  12255  efgt1p2  12258  efgt1p  12259  eflegeo  12264  eirraplem  12340  dvdsmodexp  12358  dvdsmod  12425  3dvds  12427  bitsfzolem  12517  bitsfi  12520  bitsinv1lem  12524  bitsinv1  12525  gcdn0gt0  12551  gcdaddm  12557  gcdmultipled  12566  bezoutlemle  12581  nninfctlemfo  12613  nn0seqcvgd  12615  alginv  12621  algcvg  12622  algcvga  12625  algfx  12626  eucalgval2  12627  eucalgcvga  12632  eucalg  12633  lcmcllem  12641  lcmid  12654  mulgcddvds  12668  divgcdcoprmex  12676  cncongr1  12677  cncongr2  12678  phiprmpw  12796  modprm0  12829  pcpremul  12868  pceu  12870  pcmul  12876  pcqmul  12878  pcge0  12888  pcdvdsb  12895  pcneg  12900  pcgcd1  12903  pc2dvds  12905  pcz  12907  dvdsprmpweqle  12912  qexpz  12927  4sqlemafi  12970  4sqlem11  12976  ennnfonelemjn  13025  ennnfonelemh  13027  ennnfonelem0  13028  ennnfonelem1  13030  ennnfonelemom  13031  ennnfonelemkh  13035  ennnfonelemhf1o  13036  ennnfonelemex  13037  ennnfonelemrn  13042  ennnfonelemnn0  13045  ctinfomlemom  13050  mulgval  13711  mulgfng  13713  subgmulg  13777  elply2  15462  plyf  15464  elplyd  15468  ply1termlem  15469  plyaddlem1  15474  plymullem1  15475  plymullem  15477  plycoeid3  15484  plycolemc  15485  plycjlemc  15487  plycn  15489  plyrecj  15490  dvply1  15492  sgmppw  15719  0sgmppw  15720  mersenne  15724  lgsval  15736  lgsfvalg  15737  lgscllem  15739  lgsval2lem  15742  lgsneg1  15757  lgsne0  15770  lgsquad3  15816  wksfval  16176  wlkex  16179  iswlkg  16183  012of  16609  2o01f  16610  isomninnlem  16651  iswomninnlem  16670  ismkvnnlem  16673  dceqnconst  16681  dcapnconst  16682