Theorem 0zd 12614

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  0cc0 11111  ℤcz 12602

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-1cn 11169  ax-addrcl 11172  ax-rnegex 11182  ax-cnre 11184

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 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7419  df-neg 11455  df-z 12603

This theorem is used by:  fzctr  13680  fzosubel3  13767  bcval5  14367  snopiswrd  14573  wrdsymb0  14599  ccatsymb  14633  swrdspsleq  14720  pfxnd  14742  pfxccatin12lem1  14782  swrdccat  14789  repswswrd  14840  eqwrds3  15017  fzomaxdiflem  15413  fsumzcl  15804  isumnn0nn  15914  climcndslem1  15921  climcnds  15923  harmonic  15931  geolim  15942  geolim2  15943  geoisum  15949  geoisumr  15950  mertenslem1  15956  mertenslem2  15957  mertens  15958  risefacval2  16082  fallfacval2  16083  binomfallfaclem2  16111  bpolydiflem  16125  eff  16152  efcvg  16156  reefcl  16158  efcj  16163  eftlub  16182  effsumlt  16184  eflegeo  16194  eirrlem  16277  ruclem6  16308  dvdsmodexp  16335  dvdsmod  16404  pwp1fsum  16466  bitsinv1lem  16516  sadcf  16528  sadadd3  16536  smupf  16553  gcdmultipled  16609  alginv  16650  algcvg  16651  algcvga  16654  algfx  16655  eucalgcvga  16661  eucalg  16662  lcmftp  16711  phiprmpw  16852  iserodd  16912  pcpre1  16919  qexpz  16978  prmreclem4  16996  vdwapun  17051  chnpolfz  18706  smndex2dnrinv  19000  odf1  19655  ablsimpgfindlem1  20202  srgbinomlem4  20334  pzriprnglem5  21664  pzriprnglem8  21667  pzriprnglem10  21669  pzriprnglem11  21670  pzriprng1ALT  21675  psrbagres  22109  evlslem1  22262  evlsvvvallem  22271  selvvvval  22322  psdmul  22358  cpmadugsumlemF  23062  dvnff  26111  dgrcl  26419  dgrub  26420  dgrlb  26422  elqaalem2  26510  elqaalem3  26511  geolim3  26531  tayl0  26554  dvtaylp  26562  radcnvlem1  26605  radcnvlem3  26607  radcnv0  26608  radcnvlt2  26611  pserulm  26614  psercn2  26615  pserdvlem2  26620  pserdv2  26622  abelthlem4  26626  abelthlem5  26627  abelthlem6  26628  abelthlem7  26630  abelthlem8  26631  abelthlem9  26632  cos02pilt1  26720  cosne0  26723  logtayl  26854  leibpi  27136  leibpisum  27137  log2cnv  27138  log2tlbnd  27139  basellem3  27276  dchrptlem2  27458  bcmono  27470  lgsne0  27528  crctcshwlkn0lem3  30190  fzo0opth  33177  pfxlsw2ccat  33295  wrdt2ind  33298  gsumzrsum  33408  gsummulgc2  33409  gsumwrd2dccatlem  33420  cycpmco2lem7  33475  cyc3conja  33500  archiabllem1b  33535  elrgspnlem1  33585  elrgspnlem2  33586  elrgspnlem3  33587  elrgspnlem4  33588  elrgspnsubrunlem1  33590  elrgspnsubrunlem2  33591  selvply1rhmlemb  33932  esplyfval0  33977  esplyfval2  33978  esplympl  33980  esplyfval3  33985  vietadeg1  33991  constrrecl  34182  constrimcl  34183  constrmulcl  34184  constrreinvcl  34185  constrinvcl  34186  constrresqrtcl  34190  constrabscl  34191  constrsqrtcl  34192  cos9thpiminplylem1  34195  cos9thpiminplylem2  34196  cos9thpiminply  34201  cos9thpinconstrlem1  34202  oddpwdc  34768  ballotlemfval0  34910  fsum2dsub  35018  breprexplemc  35043  breprexp  35044  circlemeth  35051  fwddifnp1  36670  knoppcnlem6  37120  knoppcnlem9  37123  knoppcn  37126  knoppndvlem2  37135  knoppndvlem4  37137  knoppf  37157  itg2addnclem2  38356  lcmineqlem4  42832  lcmineqlem18  42846  aks4d1p1p2  42870  aks4d1p3  42878  aks4d1p7d1  42882  aks4d1p7  42883  aks4d1p8  42887  aks4d1p9  42888  posbezout  42900  primrootspoweq0  42906  aks6d1c1  42916  aks6d1c2lem4  42927  aks6d1c2  42930  aks6d1c5lem1  42936  aks6d1c5lem2  42938  2np3bcnp1  42944  sticksstones12a  42957  sticksstones22  42968  aks6d1c6lem3  42972  aks6d1c6lem4  42973  aks6d1c6isolem1  42974  aks6d1c6lem5  42977  bcled  42978  bcle2d  42979  aks6d1c7lem1  42980  aks6d1c7lem2  42981  evlselvlem  43353  evlselv  43354  mhphf  43362  fltnltalem  43427  rmynn  43716  jm2.24nn  43719  jm2.17c  43722  jm2.24  43723  acongrep  43740  acongeq  43743  jm2.18  43748  jm2.23  43756  jm2.20nn  43757  jm2.27a  43765  jm2.27c  43767  rmydioph  43774  hashnzfz  45063  bccbc  45088  binomcxplemnn0  45092  binomcxplemrat  45093  binomcxplemnotnn0  45099  mccllem  46346  expfac  46404  0cnv  46489  lmbr3v  46492  sinaover2ne0  46615  dvnmul  46690  dvnprodlem1  46693  dvnprodlem2  46694  stoweidlem11  46758  stoweidlem26  46773  stoweidlem34  46781  stirlinglem5  46825  fourierdlem11  46865  fourierdlem12  46866  fourierdlem14  46868  fourierdlem15  46869  fourierdlem24  46878  fourierdlem25  46879  fourierdlem36  46890  fourierdlem37  46891  fourierdlem41  46895  fourierdlem48  46901  fourierdlem49  46902  fourierdlem50  46903  fourierdlem64  46917  fourierdlem69  46922  fourierdlem73  46926  fourierdlem79  46932  fourierdlem81  46934  fourierdlem92  46945  fourierdlem93  46946  fourierdlem111  46964  elaa2lem  46980  etransclem3  46984  etransclem7  46988  etransclem10  46991  etransclem24  47005  etransclem27  47008  etransclem35  47016  etransclem44  47025  etransclem46  47027  etransclem47  47028  etransclem48  47029  natglobalincr  47626  chnsubseqwl  47628  chnsubseq  47629  2ffzoeq  48098  iccpartigtl  48205  iccpartltu  48207  iccpartgt  48209  0even  49035  2zrngamgm  49043  altgsumbcALT  49166  expnegico01  49331  dig0  49419  nn0sumshdiglem2  49435