Theorem 0zd 9332

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

Syntax hints:   → wi 4   ∈ wcel 2164  0cc0 7874  ℤcz 9320

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-1re 7968  ax-addrcl 7971  ax-rnegex 7983

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-rab 2481  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263  df-ov 5922  df-neg 8195  df-z 9321

This theorem is referenced by:  fzctr  10202  fzosubel3  10266  frecfzennn  10500  frechashgf1o  10502  0tonninf  10514  1tonninf  10515  exp3val  10615  exp0  10617  bcval  10823  bccmpl  10828  bcval5  10837  bcpasc  10840  bccl  10841  hashcl  10855  hashfiv01gt1  10856  hashfz1  10857  hashen  10858  fihashneq0  10868  omgadd  10876  fihashdom  10877  fiubz  10903  fnfz0hash  10906  ffzo0hash  10908  wrdval  10920  snopiswrd  10927  wrdsymb0  10949  fzomaxdiflem  11259  fsumzcl  11548  fisum0diag  11587  fisum0diag2  11593  binomlem  11629  binom1dif  11633  isumnn0nn  11639  expcnvre  11649  explecnv  11651  pwm1geoserap1  11654  geolim  11657  geolim2  11658  geo2sum  11660  geoisum  11663  geoisumr  11664  mertenslemub  11680  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  fprod0diagfz  11774  eftcl  11800  efval  11807  eff  11809  efcvg  11812  efcvgfsum  11813  reefcl  11814  ege2le3  11817  efcj  11819  efaddlem  11820  eftlub  11836  effsumlt  11838  efgt1p2  11841  efgt1p  11842  eflegeo  11847  eirraplem  11923  dvdsmodexp  11941  dvdsmod  12007  gcdn0gt0  12118  gcdaddm  12124  gcdmultipled  12133  bezoutlemle  12148  nninfctlemfo  12180  nn0seqcvgd  12182  alginv  12188  algcvg  12189  algcvga  12192  algfx  12193  eucalgval2  12194  eucalgcvga  12199  eucalg  12200  lcmcllem  12208  lcmid  12221  mulgcddvds  12235  divgcdcoprmex  12243  cncongr1  12244  cncongr2  12245  phiprmpw  12363  modprm0  12395  pcpremul  12434  pceu  12436  pcmul  12442  pcqmul  12444  pcge0  12454  pcdvdsb  12461  pcneg  12466  pcgcd1  12469  pc2dvds  12471  pcz  12473  dvdsprmpweqle  12478  qexpz  12493  4sqlemafi  12536  4sqlem11  12542  ennnfonelemjn  12562  ennnfonelemh  12564  ennnfonelem0  12565  ennnfonelem1  12567  ennnfonelemom  12568  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ennnfonelemex  12574  ennnfonelemrn  12579  ennnfonelemnn0  12582  ctinfomlemom  12587  mulgval  13195  mulgfng  13197  subgmulg  13261  elply2  14914  plyf  14916  elplyd  14920  ply1termlem  14921  plyaddlem1  14926  plymullem1  14927  plymullem  14929  plycolemc  14936  plycjlemc  14938  plycn  14940  plyrecj  14941  dvply1  14943  lgsval  15161  lgsfvalg  15162  lgscllem  15164  lgsval2lem  15167  lgsneg1  15182  lgsne0  15195  lgsquad3  15241  012of  15556  2o01f  15557  isomninnlem  15590  iswomninnlem  15609  ismkvnnlem  15612  dceqnconst  15620  dcapnconst  15621