Theorem 0zd 9667

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

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

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 8279  ax-addrcl 8282  ax-rnegex 8294

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 4132  df-iota 5340  df-fv 5388  df-ov 6091  df-neg 8507  df-z 9656

This theorem is used by:  fzctr  10557  fzosubel3  10631  frecfzennn  10884  frechashgf1o  10886  0tonninf  10898  1tonninf  10899  exp3val  10999  exp0  11001  nn0sqdc  11168  bcval  11209  bccmpl  11214  bcval5  11223  bcpasc  11226  bccl  11227  hashcl  11242  hashfiv01gt1  11243  hashfz1  11244  hashen  11245  fihashneq0  11255  omgadd  11264  fihashdom  11265  fiubz  11294  fnfz0hash  11297  ffzo0hash  11299  hashfibc  11305  wrdval  11329  snopiswrd  11336  wrdsymb0  11359  ccatfvalfi  11382  ccatcl  11383  ccatlen  11385  ccatsymb  11392  fzowrddc  11441  swrdval  11442  swrdspsleq  11461  pfxval  11468  fnpfx  11471  pfxclg  11472  pfxnd  11483  pfxwrdsymbg  11484  pfxccatin12lem1  11522  pfxccatin12  11527  swrdccat  11529  fzomaxdiflem  11901  fsumzcl  12194  fisum0diag  12233  fisum0diag2  12239  binomlem  12275  binom1dif  12279  isumnn0nn  12285  expcnvre  12295  explecnv  12297  pwm1geoserap1  12300  geolim  12303  geolim2  12304  geo2sum  12306  geoisum  12309  geoisumr  12310  mertenslemub  12326  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  fprod0diagfz  12420  eftcl  12446  efval  12453  eff  12455  efcvg  12458  efcvgfsum  12459  reefcl  12460  ege2le3  12463  efcj  12465  efaddlem  12466  eftlub  12482  effsumlt  12484  efgt1p2  12487  efgt1p  12488  eflegeo  12493  eirraplem  12569  dvdsmodexp  12587  dvdsmod  12654  3dvds  12656  bitsfzolem  12746  bitsfi  12749  bitsinv1lem  12753  bitsinv1  12754  gcdn0gt0  12780  gcdaddm  12786  gcdmultipled  12795  bezoutlemle  12810  nninfctlemfo  12842  nn0seqcvgd  12844  alginv  12850  algcvg  12851  algcvga  12854  algfx  12855  eucalgval2  12856  eucalgcvga  12861  eucalg  12862  lcmcllem  12870  lcmid  12883  mulgcddvds  12897  divgcdcoprmex  12905  cncongr1  12906  cncongr2  12907  phiprmpw  13029  modprm0  13062  pcpremul  13101  pceu  13103  pcmul  13109  pcqmul  13111  pcge0  13121  pcdvdsb  13128  pcneg  13133  pcgcd1  13136  pc2dvds  13138  pcz  13140  dvdsprmpweqle  13145  qexpz  13160  4sqlemafi  13203  4sqlem11  13209  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemfval0  13293  ballotfilemiex  13302  ennnfonelemjn  13351  ennnfonelemh  13353  ennnfonelem0  13354  ennnfonelem1  13356  ennnfonelemom  13357  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ennnfonelemex  13363  ennnfonelemrn  13368  ennnfonelemnn0  13371  ctinfomlemom  13376  mulgval  13984  mulgfng  13986  subgmulg  14050  psrbaglefifi  15172  elply2  15961  plyf  15963  elplyd  15967  ply1termlem  15968  plyaddlem1  15973  plymullem1  15974  plymullem  15976  plycoeid3  15983  plycolemc  15984  plycjlemc  15986  plycn  15988  plyrecj  15989  dvply1  15991  log2tlbndlog2  16220  log2ublem2  16222  log2ublog2  16224  birthdaylem3  16227  sgmppw  16286  0sgmppw  16287  chtublem  16295  mersenne  16297  bcmono  16304  lgsval  16328  lgsfvalg  16329  lgscllem  16331  lgsval2lem  16334  lgsneg1  16349  lgsne0  16362  lgsquad3  16408  wksfval  16768  wlkex  16771  iswlkg  16775  depindlem1  16952  012of  17228  2o01f  17229  isomninnlem  17285  iswomninnlem  17306  ismkvnnlem  17309  dceqnconst  17317  dcapnconst  17318