Theorem 0zd 9469

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

Syntax hints:   → wi 4   ∈ wcel 2200  0cc0 8010  ℤcz 9457

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8104  ax-addrcl 8107  ax-rnegex 8119

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010  df-neg 8331  df-z 9458

This theorem is referenced by:  fzctr  10341  fzosubel3  10414  frecfzennn  10660  frechashgf1o  10662  0tonninf  10674  1tonninf  10675  exp3val  10775  exp0  10777  bcval  10983  bccmpl  10988  bcval5  10997  bcpasc  11000  bccl  11001  hashcl  11015  hashfiv01gt1  11016  hashfz1  11017  hashen  11018  fihashneq0  11028  omgadd  11036  fihashdom  11037  fiubz  11064  fnfz0hash  11067  ffzo0hash  11069  wrdval  11087  snopiswrd  11094  wrdsymb0  11117  ccatfvalfi  11140  ccatcl  11141  ccatlen  11143  ccatsymb  11150  fzowrddc  11194  swrdval  11195  swrdspsleq  11214  pfxval  11221  fnpfx  11224  pfxclg  11225  pfxnd  11236  pfxwrdsymbg  11237  pfxccatin12lem1  11275  pfxccatin12  11280  swrdccat  11282  fzomaxdiflem  11638  fsumzcl  11928  fisum0diag  11967  fisum0diag2  11973  binomlem  12009  binom1dif  12013  isumnn0nn  12019  expcnvre  12029  explecnv  12031  pwm1geoserap1  12034  geolim  12037  geolim2  12038  geo2sum  12040  geoisum  12043  geoisumr  12044  mertenslemub  12060  mertenslemi1  12061  mertenslem2  12062  mertensabs  12063  fprod0diagfz  12154  eftcl  12180  efval  12187  eff  12189  efcvg  12192  efcvgfsum  12193  reefcl  12194  ege2le3  12197  efcj  12199  efaddlem  12200  eftlub  12216  effsumlt  12218  efgt1p2  12221  efgt1p  12222  eflegeo  12227  eirraplem  12303  dvdsmodexp  12321  dvdsmod  12388  3dvds  12390  bitsfzolem  12480  bitsfi  12483  bitsinv1lem  12487  bitsinv1  12488  gcdn0gt0  12514  gcdaddm  12520  gcdmultipled  12529  bezoutlemle  12544  nninfctlemfo  12576  nn0seqcvgd  12578  alginv  12584  algcvg  12585  algcvga  12588  algfx  12589  eucalgval2  12590  eucalgcvga  12595  eucalg  12596  lcmcllem  12604  lcmid  12617  mulgcddvds  12631  divgcdcoprmex  12639  cncongr1  12640  cncongr2  12641  phiprmpw  12759  modprm0  12792  pcpremul  12831  pceu  12833  pcmul  12839  pcqmul  12841  pcge0  12851  pcdvdsb  12858  pcneg  12863  pcgcd1  12866  pc2dvds  12868  pcz  12870  dvdsprmpweqle  12875  qexpz  12890  4sqlemafi  12933  4sqlem11  12939  ennnfonelemjn  12988  ennnfonelemh  12990  ennnfonelem0  12991  ennnfonelem1  12993  ennnfonelemom  12994  ennnfonelemkh  12998  ennnfonelemhf1o  12999  ennnfonelemex  13000  ennnfonelemrn  13005  ennnfonelemnn0  13008  ctinfomlemom  13013  mulgval  13674  mulgfng  13676  subgmulg  13740  elply2  15424  plyf  15426  elplyd  15430  ply1termlem  15431  plyaddlem1  15436  plymullem1  15437  plymullem  15439  plycoeid3  15446  plycolemc  15447  plycjlemc  15449  plycn  15451  plyrecj  15452  dvply1  15454  sgmppw  15681  0sgmppw  15682  mersenne  15686  lgsval  15698  lgsfvalg  15699  lgscllem  15701  lgsval2lem  15704  lgsneg1  15719  lgsne0  15732  lgsquad3  15778  wksfval  16063  wlkex  16066  iswlkg  16070  012of  16416  2o01f  16417  isomninnlem  16458  iswomninnlem  16477  ismkvnnlem  16480  dceqnconst  16488  dcapnconst  16489