Theorem 0zd 8860

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

Syntax hints:   → wi 4   ∈ wcel 1445  0cc0 7447  ℤcz 8848

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-1re 7536  ax-addrcl 7539  ax-rnegex 7551

This theorem depends on definitions:  df-bi 116  df-3or 928  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ral 2375  df-rex 2376  df-rab 2379  df-v 2635  df-un 3017  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-br 3868  df-iota 5014  df-fv 5057  df-ov 5693  df-neg 7753  df-z 8849

This theorem is referenced by:  fzctr  9693  fzosubel3  9756  frecfzennn  9982  frechashgf1o  9984  0tonninf  9994  1tonninf  9995  exp3val  10088  exp0  10090  bcval  10288  bccmpl  10293  bcval5  10302  bcpasc  10305  bccl  10306  hashcl  10320  hashfiv01gt1  10321  hashfz1  10322  hashen  10323  fihashneq0  10334  omgadd  10341  fihashdom  10342  fnfz0hash  10368  ffzo0hash  10370  fzomaxdiflem  10676  fsumzcl  10960  fisum0diag  10999  fisum0diag2  11005  binomlem  11041  binom1dif  11045  isumnn0nn  11051  expcnvre  11061  explecnv  11063  pwm1geoserap1  11066  geolim  11069  geolim2  11070  geo2sum  11072  geoisum  11075  geoisumr  11076  mertenslemub  11092  mertenslemi1  11093  mertenslem2  11094  mertensabs  11095  eftcl  11108  efval  11115  eff  11117  efcvg  11120  efcvgfsum  11121  reefcl  11122  ege2le3  11125  efcj  11127  efaddlem  11128  eftlub  11144  effsumlt  11146  efgt1p2  11149  efgt1p  11150  eflegeo  11156  eirraplem  11228  dvdsmod  11305  gcdn0gt0  11411  gcdaddm  11417  bezoutlemle  11439  nn0seqcvgd  11465  alginv  11471  algcvg  11472  algcvga  11475  algfx  11476  eucalgval2  11477  eucalgcvga  11482  eucalg  11483  lcmcllem  11491  lcmid  11504  mulgcddvds  11518  divgcdcoprmex  11526  cncongr1  11527  cncongr2  11528  phiprmpw  11640