Theorem 0zd 12625

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

Syntax hints:   → wi 4   ∈ wcel 2108  0cc0 11155  ℤcz 12613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-addrcl 11216  ax-rnegex 11226  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-neg 11495  df-z 12614

This theorem is referenced by:  fzctr  13680  fzosubel3  13765  bcval5  14357  snopiswrd  14561  wrdsymb0  14587  ccatsymb  14620  swrdspsleq  14703  pfxnd  14725  pfxccatin12lem1  14766  swrdccat  14773  repswswrd  14822  eqwrds3  15000  fzomaxdiflem  15381  fsumzcl  15771  isumnn0nn  15878  climcndslem1  15885  climcnds  15887  harmonic  15895  geolim  15906  geolim2  15907  geoisum  15913  geoisumr  15914  mertenslem1  15920  mertenslem2  15921  mertens  15922  risefacval2  16046  fallfacval2  16047  binomfallfaclem2  16076  bpolydiflem  16090  eff  16117  efcvg  16121  reefcl  16123  efcj  16128  eftlub  16145  effsumlt  16147  eflegeo  16157  eirrlem  16240  ruclem6  16271  dvdsmodexp  16298  dvdsmod  16366  pwp1fsum  16428  bitsinv1lem  16478  sadcf  16490  sadadd3  16498  smupf  16515  gcdmultipled  16571  alginv  16612  algcvg  16613  algcvga  16616  algfx  16617  eucalgcvga  16623  eucalg  16624  lcmftp  16673  phiprmpw  16813  iserodd  16873  pcpre1  16880  qexpz  16939  prmreclem4  16957  vdwapun  17012  smndex2dnrinv  18928  odf1  19580  ablsimpgfindlem1  20127  srgbinomlem4  20226  pzriprnglem5  21496  pzriprnglem8  21499  pzriprnglem10  21501  pzriprnglem11  21502  pzriprng1ALT  21507  evlslem1  22106  psdmul  22170  cpmadugsumlemF  22882  dvnff  25959  dgrcl  26272  dgrub  26273  dgrlb  26275  elqaalem2  26362  elqaalem3  26363  geolim3  26381  tayl0  26403  dvtaylp  26412  radcnvlem1  26456  radcnvlem3  26458  radcnv0  26459  radcnvlt2  26462  pserulm  26465  psercn2  26466  psercn2OLD  26467  pserdvlem2  26472  pserdv2  26474  abelthlem4  26478  abelthlem5  26479  abelthlem6  26480  abelthlem7  26482  abelthlem8  26483  abelthlem9  26484  cos02pilt1  26568  cosne0  26571  logtayl  26702  leibpi  26985  leibpisum  26986  log2cnv  26987  log2tlbnd  26988  basellem3  27126  dchrptlem2  27309  bcmono  27321  lgsne0  27379  crctcshwlkn0lem3  29832  fzo0opth  32807  pfxlsw2ccat  32935  wrdt2ind  32938  gsumzrsum  33062  gsummulgc2  33063  gsumwrd2dccatlem  33069  cycpmco2lem7  33152  cyc3conja  33177  archiabllem1b  33199  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem3  33248  elrgspnlem4  33249  elrgspnsubrunlem1  33251  elrgspnsubrunlem2  33252  oddpwdc  34356  ballotlemfval0  34498  fsum2dsub  34622  breprexplemc  34647  breprexp  34648  circlemeth  34655  fwddifnp1  36166  knoppcnlem6  36499  knoppcnlem9  36502  knoppcn  36505  knoppndvlem2  36514  knoppndvlem4  36516  knoppf  36536  itg2addnclem2  37679  lcmineqlem4  42033  lcmineqlem18  42047  aks4d1p1p2  42071  aks4d1p3  42079  aks4d1p7d1  42083  aks4d1p7  42084  aks4d1p8  42088  aks4d1p9  42089  posbezout  42101  primrootspoweq0  42107  aks6d1c1  42117  aks6d1c2lem4  42128  aks6d1c2  42131  aks6d1c5lem1  42137  aks6d1c5lem2  42139  2np3bcnp1  42145  sticksstones12a  42158  sticksstones22  42169  aks6d1c6lem3  42173  aks6d1c6lem4  42174  aks6d1c6isolem1  42175  aks6d1c6lem5  42178  bcled  42179  bcle2d  42180  aks6d1c7lem1  42181  aks6d1c7lem2  42182  metakunt29  42234  metakunt30  42235  metakunt32  42237  metakunt33  42238  psrbagres  42556  evlsvvvallem  42571  selvvvval  42595  evlselvlem  42596  evlselv  42597  mhphf  42607  fltnltalem  42672  rmynn  42968  jm2.24nn  42971  jm2.17c  42974  jm2.24  42975  acongrep  42992  acongeq  42995  jm2.18  43000  jm2.23  43008  jm2.20nn  43009  jm2.27a  43017  jm2.27c  43019  rmydioph  43026  hashnzfz  44339  bccbc  44364  binomcxplemnn0  44368  binomcxplemrat  44369  binomcxplemnotnn0  44375  mccllem  45612  expfac  45672  0cnv  45757  lmbr3v  45760  sinaover2ne0  45883  dvnmul  45958  dvnprodlem1  45961  dvnprodlem2  45962  stoweidlem11  46026  stoweidlem26  46041  stoweidlem34  46049  stirlinglem5  46093  fourierdlem11  46133  fourierdlem12  46134  fourierdlem14  46136  fourierdlem15  46137  fourierdlem24  46146  fourierdlem25  46147  fourierdlem36  46158  fourierdlem37  46159  fourierdlem41  46163  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem64  46185  fourierdlem69  46190  fourierdlem73  46194  fourierdlem79  46200  fourierdlem81  46202  fourierdlem92  46213  fourierdlem93  46214  fourierdlem111  46232  elaa2lem  46248  etransclem3  46252  etransclem7  46256  etransclem10  46259  etransclem24  46273  etransclem27  46276  etransclem35  46284  etransclem44  46293  etransclem46  46295  etransclem47  46296  etransclem48  46297  natglobalincr  46892  2ffzoeq  47339  iccpartigtl  47410  iccpartltu  47412  iccpartgt  47414  0even  48153  2zrngamgm  48161  altgsumbcALT  48269  expnegico01  48435  dig0  48527  nn0sumshdiglem2  48543