Theorem 0zd 9366

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

Syntax hints:   → wi 4   ∈ wcel 2175  0cc0 7907  ℤcz 9354

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-1re 8001  ax-addrcl 8004  ax-rnegex 8016

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-rab 2492  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-iota 5229  df-fv 5276  df-ov 5937  df-neg 8228  df-z 9355

This theorem is referenced by:  fzctr  10237  fzosubel3  10306  frecfzennn  10552  frechashgf1o  10554  0tonninf  10566  1tonninf  10567  exp3val  10667  exp0  10669  bcval  10875  bccmpl  10880  bcval5  10889  bcpasc  10892  bccl  10893  hashcl  10907  hashfiv01gt1  10908  hashfz1  10909  hashen  10910  fihashneq0  10920  omgadd  10928  fihashdom  10929  fiubz  10955  fnfz0hash  10958  ffzo0hash  10960  wrdval  10972  snopiswrd  10979  wrdsymb0  11001  ccatfvalfi  11023  ccatcl  11024  ccatlen  11026  ccatsymb  11033  fzomaxdiflem  11342  fsumzcl  11632  fisum0diag  11671  fisum0diag2  11677  binomlem  11713  binom1dif  11717  isumnn0nn  11723  expcnvre  11733  explecnv  11735  pwm1geoserap1  11738  geolim  11741  geolim2  11742  geo2sum  11744  geoisum  11747  geoisumr  11748  mertenslemub  11764  mertenslemi1  11765  mertenslem2  11766  mertensabs  11767  fprod0diagfz  11858  eftcl  11884  efval  11891  eff  11893  efcvg  11896  efcvgfsum  11897  reefcl  11898  ege2le3  11901  efcj  11903  efaddlem  11904  eftlub  11920  effsumlt  11922  efgt1p2  11925  efgt1p  11926  eflegeo  11931  eirraplem  12007  dvdsmodexp  12025  dvdsmod  12092  3dvds  12094  bitsfzolem  12184  bitsfi  12187  bitsinv1lem  12191  bitsinv1  12192  gcdn0gt0  12218  gcdaddm  12224  gcdmultipled  12233  bezoutlemle  12248  nninfctlemfo  12280  nn0seqcvgd  12282  alginv  12288  algcvg  12289  algcvga  12292  algfx  12293  eucalgval2  12294  eucalgcvga  12299  eucalg  12300  lcmcllem  12308  lcmid  12321  mulgcddvds  12335  divgcdcoprmex  12343  cncongr1  12344  cncongr2  12345  phiprmpw  12463  modprm0  12496  pcpremul  12535  pceu  12537  pcmul  12543  pcqmul  12545  pcge0  12555  pcdvdsb  12562  pcneg  12567  pcgcd1  12570  pc2dvds  12572  pcz  12574  dvdsprmpweqle  12579  qexpz  12594  4sqlemafi  12637  4sqlem11  12643  ennnfonelemjn  12692  ennnfonelemh  12694  ennnfonelem0  12695  ennnfonelem1  12697  ennnfonelemom  12698  ennnfonelemkh  12702  ennnfonelemhf1o  12703  ennnfonelemex  12704  ennnfonelemrn  12709  ennnfonelemnn0  12712  ctinfomlemom  12717  mulgval  13376  mulgfng  13378  subgmulg  13442  elply2  15125  plyf  15127  elplyd  15131  ply1termlem  15132  plyaddlem1  15137  plymullem1  15138  plymullem  15140  plycoeid3  15147  plycolemc  15148  plycjlemc  15150  plycn  15152  plyrecj  15153  dvply1  15155  sgmppw  15382  0sgmppw  15383  mersenne  15387  lgsval  15399  lgsfvalg  15400  lgscllem  15402  lgsval2lem  15405  lgsneg1  15420  lgsne0  15433  lgsquad3  15479  012of  15794  2o01f  15795  isomninnlem  15833  iswomninnlem  15852  ismkvnnlem  15855  dceqnconst  15863  dcapnconst  15864