Theorem 0zd 12743

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  0cc0 11237  ℤcz 12731

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11295  ax-addrcl 11298  ax-rnegex 11308  ax-cnre 11310

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6518  df-fv 6572  df-ov 7452  df-neg 11581  df-z 12732

This theorem is used by:  fzctr  13812  fzosubel3  13899  bcval5  14501  snopiswrd  14707  wrdsymb0  14733  ccatsymb  14767  swrdspsleq  14855  pfxnd  14877  pfxccatin12lem1  14917  swrdccat  14924  repswswrd  14975  eqwrds3  15155  fzomaxdiflem  15551  fsumzcl  15942  isumnn0nn  16052  climcndslem1  16059  climcnds  16061  harmonic  16069  geolim  16080  geolim2  16081  geoisum  16087  geoisumr  16088  mertenslem1  16094  mertenslem2  16095  mertens  16096  risefacval2  16218  fallfacval2  16219  binomfallfaclem2  16247  bpolydiflem  16261  eff  16288  efcvg  16292  reefcl  16294  efcj  16299  eftlub  16318  effsumlt  16320  eflegeo  16330  eirrlem  16413  ruclem6  16444  dvdsmodexp  16471  dvdsmod  16540  pwp1fsum  16602  bitsinv1lem  16652  sadcf  16664  sadadd3  16672  smupf  16689  gcdmultipled  16748  alginv  16791  algcvg  16792  algcvga  16795  algfx  16796  eucalgcvga  16802  eucalg  16803  lcmftp  16852  phiprmpw  16994  iserodd  17054  pcpre1  17061  qexpz  17120  prmreclem4  17138  vdwapun  17193  chnpolfz  18848  smndex2dnrinv  19155  odf1  19818  ablsimpgfindlem1  20365  srgbinomlem4  20497  pzriprnglem5  21835  pzriprnglem8  21838  pzriprnglem10  21840  pzriprnglem11  21841  pzriprng1ALT  21846  psrbagres  22282  evlslem1  22435  evlsvvvallem  22444  selvvvval  22495  psdmul  22531  cpmadugsumlemF  23238  dvnff  26287  dgrcl  26596  dgrub  26597  dgrlb  26599  elqaalem2  26689  elqaalem3  26690  geolim3  26712  tayl0  26735  dvtaylp  26743  radcnvlem1  26786  radcnvlem3  26788  radcnv0  26789  radcnvlt2  26792  pserulm  26795  psercn2  26796  pserdvlem2  26801  pserdv2  26803  abelthlem4  26807  abelthlem5  26808  abelthlem6  26809  abelthlem7  26811  abelthlem8  26812  abelthlem9  26813  cos02pilt1  26900  cosne0  26903  logtayl  27034  leibpi  27316  leibpisum  27317  log2cnv  27318  log2tlbnd  27319  basellem3  27456  dchrptlem2  27638  bcmono  27650  lgsne0  27708  crctcshwlkn0lem3  30447  fzo0opth  33481  pfxlsw2ccat  33599  wrdt2ind  33602  gsumzrsum  33715  gsummulgc2  33716  gsumwrd2dccatlem  33727  cycpmco2lem7  33782  cyc3conja  33807  archiabllem1b  33842  elrgspnlem1  33892  elrgspnlem2  33893  elrgspnlem3  33894  elrgspnlem4  33895  elrgspnsubrunlem1  33897  elrgspnsubrunlem2  33898  selvply1rhmlemb  34255  esplyfval0  34300  esplyfval2  34301  esplympl  34303  esplyfval3  34308  vietadeg1  34314  constrrecl  34505  constrimcl  34506  constrmulcl  34507  constrreinvcl  34508  constrinvcl  34509  constrresqrtcl  34513  constrabscl  34514  constrsqrtcl  34515  cos9thpiminplylem1  34518  cos9thpiminplylem2  34519  cos9thpiminply  34524  cos9thpinconstrlem1  34525  oddpwdc  35090  ballotlemfval0  35232  fsum2dsub  35340  breprexplemc  35365  breprexp  35366  circlemeth  35373  fwddifnp1  37138  knoppcnlem6  37572  knoppcnlem9  37575  knoppcn  37578  knoppndvlem2  37587  knoppndvlem4  37589  knoppf  37609  itg2addnclem2  38851  lcmineqlem4  43341  lcmineqlem18  43355  aks4d1p1p2  43379  aks4d1p3  43387  aks4d1p7d1  43391  aks4d1p7  43392  aks4d1p8  43396  aks4d1p9  43397  posbezout  43409  primrootspoweq0  43415  aks6d1c1  43425  aks6d1c2lem4  43436  aks6d1c2  43439  aks6d1c5lem1  43445  aks6d1c5lem2  43447  2np3bcnp1  43453  sticksstones12a  43466  sticksstones22  43477  aks6d1c6lem3  43481  aks6d1c6lem4  43482  aks6d1c6isolem1  43483  aks6d1c6lem5  43486  bcled  43487  bcle2d  43488  aks6d1c7lem1  43489  aks6d1c7lem2  43490  evlselvlem  43876  evlselv  43877  mhphf  43885  fltnltalem  43933  rmynn  44223  jm2.24nn  44226  jm2.17c  44229  jm2.24  44230  acongrep  44247  acongeq  44250  jm2.18  44255  jm2.23  44263  jm2.20nn  44264  jm2.27a  44272  jm2.27c  44274  rmydioph  44281  hashnzfz  45559  bccbc  45584  binomcxplemnn0  45588  binomcxplemrat  45589  binomcxplemnotnn0  45595  mccllem  46876  expfac  46934  0cnv  47019  lmbr3v  47022  sinaover2ne0  47145  dvnmul  47220  dvnprodlem1  47223  dvnprodlem2  47224  stoweidlem11  47288  stoweidlem26  47303  stoweidlem34  47311  stirlinglem5  47355  fourierdlem11  47395  fourierdlem12  47396  fourierdlem14  47398  fourierdlem15  47399  fourierdlem24  47408  fourierdlem25  47409  fourierdlem36  47420  fourierdlem37  47421  fourierdlem41  47425  fourierdlem48  47431  fourierdlem49  47432  fourierdlem50  47433  fourierdlem64  47447  fourierdlem69  47452  fourierdlem73  47456  fourierdlem79  47462  fourierdlem81  47464  fourierdlem92  47475  fourierdlem93  47476  fourierdlem111  47494  elaa2lem  47510  etransclem3  47514  etransclem7  47518  etransclem10  47521  etransclem24  47535  etransclem27  47538  etransclem35  47546  etransclem44  47555  etransclem46  47557  etransclem47  47558  etransclem48  47559  chnsubseqwl  48156  chnsubseq  48157  2ffzoeq  48665  iccpartigtl  48772  iccpartltu  48774  iccpartgt  48776  0even  49601  2zrngamgm  49609  zellaz  49723  adcnmulzlaz  49725  altgsumbcALT  49790  expnegico01  49955  dig0  50043  nn0sumshdiglem2  50059