Theorem 0zd 9491

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

Syntax hints:   → wi 4   ∈ wcel 2202  0cc0 8032  ℤcz 9479

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 8126  ax-addrcl 8129  ax-rnegex 8141

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 6021  df-neg 8353  df-z 9480

This theorem is referenced by:  fzctr  10368  fzosubel3  10442  frecfzennn  10689  frechashgf1o  10691  0tonninf  10703  1tonninf  10704  exp3val  10804  exp0  10806  bcval  11012  bccmpl  11017  bcval5  11026  bcpasc  11029  bccl  11030  hashcl  11044  hashfiv01gt1  11045  hashfz1  11046  hashen  11047  fihashneq0  11057  omgadd  11066  fihashdom  11067  fiubz  11094  fnfz0hash  11097  ffzo0hash  11099  wrdval  11120  snopiswrd  11127  wrdsymb0  11150  ccatfvalfi  11173  ccatcl  11174  ccatlen  11176  ccatsymb  11183  fzowrddc  11232  swrdval  11233  swrdspsleq  11252  pfxval  11259  fnpfx  11262  pfxclg  11263  pfxnd  11274  pfxwrdsymbg  11275  pfxccatin12lem1  11313  pfxccatin12  11318  swrdccat  11320  fzomaxdiflem  11690  fsumzcl  11981  fisum0diag  12020  fisum0diag2  12026  binomlem  12062  binom1dif  12066  isumnn0nn  12072  expcnvre  12082  explecnv  12084  pwm1geoserap1  12087  geolim  12090  geolim2  12091  geo2sum  12093  geoisum  12096  geoisumr  12097  mertenslemub  12113  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  fprod0diagfz  12207  eftcl  12233  efval  12240  eff  12242  efcvg  12245  efcvgfsum  12246  reefcl  12247  ege2le3  12250  efcj  12252  efaddlem  12253  eftlub  12269  effsumlt  12271  efgt1p2  12274  efgt1p  12275  eflegeo  12280  eirraplem  12356  dvdsmodexp  12374  dvdsmod  12441  3dvds  12443  bitsfzolem  12533  bitsfi  12536  bitsinv1lem  12540  bitsinv1  12541  gcdn0gt0  12567  gcdaddm  12573  gcdmultipled  12582  bezoutlemle  12597  nninfctlemfo  12629  nn0seqcvgd  12631  alginv  12637  algcvg  12638  algcvga  12641  algfx  12642  eucalgval2  12643  eucalgcvga  12648  eucalg  12649  lcmcllem  12657  lcmid  12670  mulgcddvds  12684  divgcdcoprmex  12692  cncongr1  12693  cncongr2  12694  phiprmpw  12812  modprm0  12845  pcpremul  12884  pceu  12886  pcmul  12892  pcqmul  12894  pcge0  12904  pcdvdsb  12911  pcneg  12916  pcgcd1  12919  pc2dvds  12921  pcz  12923  dvdsprmpweqle  12928  qexpz  12943  4sqlemafi  12986  4sqlem11  12992  ennnfonelemjn  13041  ennnfonelemh  13043  ennnfonelem0  13044  ennnfonelem1  13046  ennnfonelemom  13047  ennnfonelemkh  13051  ennnfonelemhf1o  13052  ennnfonelemex  13053  ennnfonelemrn  13058  ennnfonelemnn0  13061  ctinfomlemom  13066  mulgval  13727  mulgfng  13729  subgmulg  13793  elply2  15478  plyf  15480  elplyd  15484  ply1termlem  15485  plyaddlem1  15490  plymullem1  15491  plymullem  15493  plycoeid3  15500  plycolemc  15501  plycjlemc  15503  plycn  15505  plyrecj  15506  dvply1  15508  sgmppw  15735  0sgmppw  15736  mersenne  15740  lgsval  15752  lgsfvalg  15753  lgscllem  15755  lgsval2lem  15758  lgsneg1  15773  lgsne0  15786  lgsquad3  15832  wksfval  16192  wlkex  16195  iswlkg  16199  depindlem1  16376  012of  16643  2o01f  16644  isomninnlem  16685  iswomninnlem  16705  ismkvnnlem  16708  dceqnconst  16716  dcapnconst  16717