Theorem 0zd 9481

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

Syntax hints:   → wi 4   ∈ wcel 2200  0cc0 8022  ℤcz 9469

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 8116  ax-addrcl 8119  ax-rnegex 8131

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 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016  df-neg 8343  df-z 9470

This theorem is referenced by:  fzctr  10358  fzosubel3  10431  frecfzennn  10678  frechashgf1o  10680  0tonninf  10692  1tonninf  10693  exp3val  10793  exp0  10795  bcval  11001  bccmpl  11006  bcval5  11015  bcpasc  11018  bccl  11019  hashcl  11033  hashfiv01gt1  11034  hashfz1  11035  hashen  11036  fihashneq0  11046  omgadd  11055  fihashdom  11056  fiubz  11083  fnfz0hash  11086  ffzo0hash  11088  wrdval  11106  snopiswrd  11113  wrdsymb0  11136  ccatfvalfi  11159  ccatcl  11160  ccatlen  11162  ccatsymb  11169  fzowrddc  11218  swrdval  11219  swrdspsleq  11238  pfxval  11245  fnpfx  11248  pfxclg  11249  pfxnd  11260  pfxwrdsymbg  11261  pfxccatin12lem1  11299  pfxccatin12  11304  swrdccat  11306  fzomaxdiflem  11663  fsumzcl  11953  fisum0diag  11992  fisum0diag2  11998  binomlem  12034  binom1dif  12038  isumnn0nn  12044  expcnvre  12054  explecnv  12056  pwm1geoserap1  12059  geolim  12062  geolim2  12063  geo2sum  12065  geoisum  12068  geoisumr  12069  mertenslemub  12085  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  fprod0diagfz  12179  eftcl  12205  efval  12212  eff  12214  efcvg  12217  efcvgfsum  12218  reefcl  12219  ege2le3  12222  efcj  12224  efaddlem  12225  eftlub  12241  effsumlt  12243  efgt1p2  12246  efgt1p  12247  eflegeo  12252  eirraplem  12328  dvdsmodexp  12346  dvdsmod  12413  3dvds  12415  bitsfzolem  12505  bitsfi  12508  bitsinv1lem  12512  bitsinv1  12513  gcdn0gt0  12539  gcdaddm  12545  gcdmultipled  12554  bezoutlemle  12569  nninfctlemfo  12601  nn0seqcvgd  12603  alginv  12609  algcvg  12610  algcvga  12613  algfx  12614  eucalgval2  12615  eucalgcvga  12620  eucalg  12621  lcmcllem  12629  lcmid  12642  mulgcddvds  12656  divgcdcoprmex  12664  cncongr1  12665  cncongr2  12666  phiprmpw  12784  modprm0  12817  pcpremul  12856  pceu  12858  pcmul  12864  pcqmul  12866  pcge0  12876  pcdvdsb  12883  pcneg  12888  pcgcd1  12891  pc2dvds  12893  pcz  12895  dvdsprmpweqle  12900  qexpz  12915  4sqlemafi  12958  4sqlem11  12964  ennnfonelemjn  13013  ennnfonelemh  13015  ennnfonelem0  13016  ennnfonelem1  13018  ennnfonelemom  13019  ennnfonelemkh  13023  ennnfonelemhf1o  13024  ennnfonelemex  13025  ennnfonelemrn  13030  ennnfonelemnn0  13033  ctinfomlemom  13038  mulgval  13699  mulgfng  13701  subgmulg  13765  elply2  15449  plyf  15451  elplyd  15455  ply1termlem  15456  plyaddlem1  15461  plymullem1  15462  plymullem  15464  plycoeid3  15471  plycolemc  15472  plycjlemc  15474  plycn  15476  plyrecj  15477  dvply1  15479  sgmppw  15706  0sgmppw  15707  mersenne  15711  lgsval  15723  lgsfvalg  15724  lgscllem  15726  lgsval2lem  15729  lgsneg1  15744  lgsne0  15757  lgsquad3  15803  wksfval  16119  wlkex  16122  iswlkg  16126  012of  16528  2o01f  16529  isomninnlem  16570  iswomninnlem  16589  ismkvnnlem  16592  dceqnconst  16600  dcapnconst  16601