Theorem 0zd 12566

Description: Zero is an integer, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
0zd	⊢ (𝜑 → 0 ∈ ℤ)

Proof of Theorem 0zd

Step	Hyp	Ref	Expression
1		0z 12565	. 2 ⊢ 0 ∈ ℤ
2	1	a1i 11	1 ⊢ (𝜑 → 0 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2106  0cc0 11106  ℤcz 12554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-1cn 11164  ax-addrcl 11167  ax-rnegex 11177  ax-cnre 11179

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-neg 11443  df-z 12555

This theorem is referenced by:  fzctr  13609  fzosubel3  13689  bcval5  14274  snopiswrd  14469  wrdsymb0  14495  ccatsymb  14528  swrdspsleq  14611  pfxnd  14633  pfxccatin12lem1  14674  swrdccat  14681  repswswrd  14730  eqwrds3  14908  fzomaxdiflem  15285  fsumzcl  15677  isumnn0nn  15784  climcndslem1  15791  climcnds  15793  harmonic  15801  geolim  15812  geolim2  15813  geoisum  15819  geoisumr  15820  mertenslem1  15826  mertenslem2  15827  mertens  15828  risefacval2  15950  fallfacval2  15951  binomfallfaclem2  15980  bpolydiflem  15994  eff  16021  efcvg  16024  reefcl  16026  efcj  16031  eftlub  16048  effsumlt  16050  eflegeo  16060  eirrlem  16143  ruclem6  16174  dvdsmodexp  16201  dvdsmod  16268  pwp1fsum  16330  bitsinv1lem  16378  sadcf  16390  sadadd3  16398  smupf  16415  gcdmultipled  16472  alginv  16508  algcvg  16509  algcvga  16512  algfx  16513  eucalgcvga  16519  eucalg  16520  lcmftp  16569  phiprmpw  16705  iserodd  16764  pcpre1  16771  qexpz  16830  prmreclem4  16848  vdwapun  16903  smndex2dnrinv  18792  odf1  19424  ablsimpgfindlem1  19971  srgbinomlem4  20045  evlslem1  21636  cpmadugsumlemF  22369  dvnff  25431  dgrcl  25738  dgrub  25739  dgrlb  25741  elqaalem2  25824  elqaalem3  25825  geolim3  25843  tayl0  25865  dvtaylp  25873  radcnvlem1  25916  radcnvlem3  25918  radcnv0  25919  radcnvlt2  25922  pserulm  25925  psercn2  25926  pserdvlem2  25931  pserdv2  25933  abelthlem4  25937  abelthlem5  25938  abelthlem6  25939  abelthlem7  25941  abelthlem8  25942  abelthlem9  25943  cos02pilt1  26026  cosne0  26029  logtayl  26159  leibpi  26436  leibpisum  26437  log2cnv  26438  log2tlbnd  26439  basellem3  26576  dchrptlem2  26757  bcmono  26769  lgsne0  26827  crctcshwlkn0lem3  29055  pfxlsw2ccat  32103  wrdt2ind  32104  cycpmco2lem7  32278  cyc3conja  32303  archiabllem1b  32325  oddpwdc  33341  ballotlemfval0  33482  fsum2dsub  33607  breprexplemc  33632  breprexp  33633  circlemeth  33640  fwddifnp1  35125  gg-psercn2  35166  knoppcnlem6  35362  knoppcnlem9  35365  knoppcn  35368  knoppndvlem2  35377  knoppndvlem4  35379  knoppf  35399  itg2addnclem2  36528  lcmineqlem4  40885  lcmineqlem18  40899  aks4d1p1p2  40923  aks4d1p3  40931  aks4d1p7d1  40935  aks4d1p7  40936  aks4d1p8  40940  aks4d1p9  40941  2np3bcnp1  40948  sticksstones12a  40961  sticksstones22  40972  metakunt29  41001  metakunt30  41002  metakunt32  41004  metakunt33  41005  psrbagres  41112  evlsvvvallem  41130  selvvvval  41154  evlselvlem  41155  evlselv  41156  mhphf  41166  fltnltalem  41400  rmynn  41680  jm2.24nn  41683  jm2.17c  41686  jm2.24  41687  acongrep  41704  acongeq  41707  jm2.18  41712  jm2.23  41720  jm2.20nn  41721  jm2.27a  41729  jm2.27c  41731  rmydioph  41738  hashnzfz  43064  bccbc  43089  binomcxplemnn0  43093  binomcxplemrat  43094  binomcxplemnotnn0  43100  mccllem  44299  expfac  44359  0cnv  44444  lmbr3v  44447  sinaover2ne0  44570  dvnmul  44645  dvnprodlem1  44648  dvnprodlem2  44649  stoweidlem11  44713  stoweidlem26  44728  stoweidlem34  44736  stirlinglem5  44780  fourierdlem11  44820  fourierdlem12  44821  fourierdlem14  44823  fourierdlem15  44824  fourierdlem24  44833  fourierdlem25  44834  fourierdlem36  44845  fourierdlem37  44846  fourierdlem41  44850  fourierdlem48  44856  fourierdlem49  44857  fourierdlem50  44858  fourierdlem64  44872  fourierdlem69  44877  fourierdlem73  44881  fourierdlem79  44887  fourierdlem81  44889  fourierdlem92  44900  fourierdlem93  44901  fourierdlem111  44919  elaa2lem  44935  etransclem3  44939  etransclem7  44943  etransclem10  44946  etransclem24  44960  etransclem27  44963  etransclem35  44971  etransclem44  44980  etransclem46  44982  etransclem47  44983  etransclem48  44984  natglobalincr  45577  2ffzoeq  46022  iccpartigtl  46077  iccpartltu  46079  iccpartgt  46081  0even  46782  2zrngamgm  46790  altgsumbcALT  46982  expnegico01  47152  dig0  47245  nn0sumshdiglem2  47261