Theorem 0zd 9404

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

Syntax hints:   → wi 4   ∈ wcel 2177  0cc0 7945  ℤcz 9392

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-1re 8039  ax-addrcl 8042  ax-rnegex 8054

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-rab 2494  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-br 4052  df-iota 5241  df-fv 5288  df-ov 5960  df-neg 8266  df-z 9393

This theorem is referenced by:  fzctr  10275  fzosubel3  10347  frecfzennn  10593  frechashgf1o  10595  0tonninf  10607  1tonninf  10608  exp3val  10708  exp0  10710  bcval  10916  bccmpl  10921  bcval5  10930  bcpasc  10933  bccl  10934  hashcl  10948  hashfiv01gt1  10949  hashfz1  10950  hashen  10951  fihashneq0  10961  omgadd  10969  fihashdom  10970  fiubz  10996  fnfz0hash  10999  ffzo0hash  11001  wrdval  11019  snopiswrd  11026  wrdsymb0  11048  ccatfvalfi  11071  ccatcl  11072  ccatlen  11074  ccatsymb  11081  fzowrddc  11123  swrdval  11124  swrdspsleq  11143  pfxval  11150  fnpfx  11153  pfxclg  11154  pfxnd  11165  pfxwrdsymbg  11166  fzomaxdiflem  11498  fsumzcl  11788  fisum0diag  11827  fisum0diag2  11833  binomlem  11869  binom1dif  11873  isumnn0nn  11879  expcnvre  11889  explecnv  11891  pwm1geoserap1  11894  geolim  11897  geolim2  11898  geo2sum  11900  geoisum  11903  geoisumr  11904  mertenslemub  11920  mertenslemi1  11921  mertenslem2  11922  mertensabs  11923  fprod0diagfz  12014  eftcl  12040  efval  12047  eff  12049  efcvg  12052  efcvgfsum  12053  reefcl  12054  ege2le3  12057  efcj  12059  efaddlem  12060  eftlub  12076  effsumlt  12078  efgt1p2  12081  efgt1p  12082  eflegeo  12087  eirraplem  12163  dvdsmodexp  12181  dvdsmod  12248  3dvds  12250  bitsfzolem  12340  bitsfi  12343  bitsinv1lem  12347  bitsinv1  12348  gcdn0gt0  12374  gcdaddm  12380  gcdmultipled  12389  bezoutlemle  12404  nninfctlemfo  12436  nn0seqcvgd  12438  alginv  12444  algcvg  12445  algcvga  12448  algfx  12449  eucalgval2  12450  eucalgcvga  12455  eucalg  12456  lcmcllem  12464  lcmid  12477  mulgcddvds  12491  divgcdcoprmex  12499  cncongr1  12500  cncongr2  12501  phiprmpw  12619  modprm0  12652  pcpremul  12691  pceu  12693  pcmul  12699  pcqmul  12701  pcge0  12711  pcdvdsb  12718  pcneg  12723  pcgcd1  12726  pc2dvds  12728  pcz  12730  dvdsprmpweqle  12735  qexpz  12750  4sqlemafi  12793  4sqlem11  12799  ennnfonelemjn  12848  ennnfonelemh  12850  ennnfonelem0  12851  ennnfonelem1  12853  ennnfonelemom  12854  ennnfonelemkh  12858  ennnfonelemhf1o  12859  ennnfonelemex  12860  ennnfonelemrn  12865  ennnfonelemnn0  12868  ctinfomlemom  12873  mulgval  13533  mulgfng  13535  subgmulg  13599  elply2  15282  plyf  15284  elplyd  15288  ply1termlem  15289  plyaddlem1  15294  plymullem1  15295  plymullem  15297  plycoeid3  15304  plycolemc  15305  plycjlemc  15307  plycn  15309  plyrecj  15310  dvply1  15312  sgmppw  15539  0sgmppw  15540  mersenne  15544  lgsval  15556  lgsfvalg  15557  lgscllem  15559  lgsval2lem  15562  lgsneg1  15577  lgsne0  15590  lgsquad3  15636  012of  16069  2o01f  16070  isomninnlem  16110  iswomninnlem  16129  ismkvnnlem  16132  dceqnconst  16140  dcapnconst  16141