Theorem 0zd 9490

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

Syntax hints:   → wi 4   ∈ wcel 2202  0cc0 8031  ℤcz 9478

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 8125  ax-addrcl 8128  ax-rnegex 8140

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 6020  df-neg 8352  df-z 9479

This theorem is referenced by:  fzctr  10367  fzosubel3  10440  frecfzennn  10687  frechashgf1o  10689  0tonninf  10701  1tonninf  10702  exp3val  10802  exp0  10804  bcval  11010  bccmpl  11015  bcval5  11024  bcpasc  11027  bccl  11028  hashcl  11042  hashfiv01gt1  11043  hashfz1  11044  hashen  11045  fihashneq0  11055  omgadd  11064  fihashdom  11065  fiubz  11092  fnfz0hash  11095  ffzo0hash  11097  wrdval  11115  snopiswrd  11122  wrdsymb0  11145  ccatfvalfi  11168  ccatcl  11169  ccatlen  11171  ccatsymb  11178  fzowrddc  11227  swrdval  11228  swrdspsleq  11247  pfxval  11254  fnpfx  11257  pfxclg  11258  pfxnd  11269  pfxwrdsymbg  11270  pfxccatin12lem1  11308  pfxccatin12  11313  swrdccat  11315  fzomaxdiflem  11672  fsumzcl  11962  fisum0diag  12001  fisum0diag2  12007  binomlem  12043  binom1dif  12047  isumnn0nn  12053  expcnvre  12063  explecnv  12065  pwm1geoserap1  12068  geolim  12071  geolim2  12072  geo2sum  12074  geoisum  12077  geoisumr  12078  mertenslemub  12094  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  fprod0diagfz  12188  eftcl  12214  efval  12221  eff  12223  efcvg  12226  efcvgfsum  12227  reefcl  12228  ege2le3  12231  efcj  12233  efaddlem  12234  eftlub  12250  effsumlt  12252  efgt1p2  12255  efgt1p  12256  eflegeo  12261  eirraplem  12337  dvdsmodexp  12355  dvdsmod  12422  3dvds  12424  bitsfzolem  12514  bitsfi  12517  bitsinv1lem  12521  bitsinv1  12522  gcdn0gt0  12548  gcdaddm  12554  gcdmultipled  12563  bezoutlemle  12578  nninfctlemfo  12610  nn0seqcvgd  12612  alginv  12618  algcvg  12619  algcvga  12622  algfx  12623  eucalgval2  12624  eucalgcvga  12629  eucalg  12630  lcmcllem  12638  lcmid  12651  mulgcddvds  12665  divgcdcoprmex  12673  cncongr1  12674  cncongr2  12675  phiprmpw  12793  modprm0  12826  pcpremul  12865  pceu  12867  pcmul  12873  pcqmul  12875  pcge0  12885  pcdvdsb  12892  pcneg  12897  pcgcd1  12900  pc2dvds  12902  pcz  12904  dvdsprmpweqle  12909  qexpz  12924  4sqlemafi  12967  4sqlem11  12973  ennnfonelemjn  13022  ennnfonelemh  13024  ennnfonelem0  13025  ennnfonelem1  13027  ennnfonelemom  13028  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ennnfonelemex  13034  ennnfonelemrn  13039  ennnfonelemnn0  13042  ctinfomlemom  13047  mulgval  13708  mulgfng  13710  subgmulg  13774  elply2  15458  plyf  15460  elplyd  15464  ply1termlem  15465  plyaddlem1  15470  plymullem1  15471  plymullem  15473  plycoeid3  15480  plycolemc  15481  plycjlemc  15483  plycn  15485  plyrecj  15486  dvply1  15488  sgmppw  15715  0sgmppw  15716  mersenne  15720  lgsval  15732  lgsfvalg  15733  lgscllem  15735  lgsval2lem  15738  lgsneg1  15753  lgsne0  15766  lgsquad3  15812  wksfval  16172  wlkex  16175  iswlkg  16179  012of  16592  2o01f  16593  isomninnlem  16634  iswomninnlem  16653  ismkvnnlem  16656  dceqnconst  16664  dcapnconst  16665