Theorem 0zd 12541

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

Syntax hints:   → wi 4   ∈ wcel 2109  0cc0 11068  ℤcz 12529

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-addrcl 11129  ax-rnegex 11139  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-neg 11408  df-z 12530

This theorem is referenced by:  fzctr  13601  fzosubel3  13687  bcval5  14283  snopiswrd  14488  wrdsymb0  14514  ccatsymb  14547  swrdspsleq  14630  pfxnd  14652  pfxccatin12lem1  14693  swrdccat  14700  repswswrd  14749  eqwrds3  14927  fzomaxdiflem  15309  fsumzcl  15701  isumnn0nn  15808  climcndslem1  15815  climcnds  15817  harmonic  15825  geolim  15836  geolim2  15837  geoisum  15843  geoisumr  15844  mertenslem1  15850  mertenslem2  15851  mertens  15852  risefacval2  15976  fallfacval2  15977  binomfallfaclem2  16006  bpolydiflem  16020  eff  16047  efcvg  16051  reefcl  16053  efcj  16058  eftlub  16077  effsumlt  16079  eflegeo  16089  eirrlem  16172  ruclem6  16203  dvdsmodexp  16230  dvdsmod  16299  pwp1fsum  16361  bitsinv1lem  16411  sadcf  16423  sadadd3  16431  smupf  16448  gcdmultipled  16504  alginv  16545  algcvg  16546  algcvga  16549  algfx  16550  eucalgcvga  16556  eucalg  16557  lcmftp  16606  phiprmpw  16746  iserodd  16806  pcpre1  16813  qexpz  16872  prmreclem4  16890  vdwapun  16945  smndex2dnrinv  18842  odf1  19492  ablsimpgfindlem1  20039  srgbinomlem4  20138  pzriprnglem5  21395  pzriprnglem8  21398  pzriprnglem10  21400  pzriprnglem11  21401  pzriprng1ALT  21406  evlslem1  21989  psdmul  22053  cpmadugsumlemF  22763  dvnff  25825  dgrcl  26138  dgrub  26139  dgrlb  26141  elqaalem2  26228  elqaalem3  26229  geolim3  26247  tayl0  26269  dvtaylp  26278  radcnvlem1  26322  radcnvlem3  26324  radcnv0  26325  radcnvlt2  26328  pserulm  26331  psercn2  26332  psercn2OLD  26333  pserdvlem2  26338  pserdv2  26340  abelthlem4  26344  abelthlem5  26345  abelthlem6  26346  abelthlem7  26348  abelthlem8  26349  abelthlem9  26350  cos02pilt1  26435  cosne0  26438  logtayl  26569  leibpi  26852  leibpisum  26853  log2cnv  26854  log2tlbnd  26855  basellem3  26993  dchrptlem2  27176  bcmono  27188  lgsne0  27246  crctcshwlkn0lem3  29742  fzo0opth  32728  pfxlsw2ccat  32872  wrdt2ind  32875  gsumzrsum  32999  gsummulgc2  33000  gsumwrd2dccatlem  33006  cycpmco2lem7  33089  cyc3conja  33114  archiabllem1b  33146  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem3  33195  elrgspnlem4  33196  elrgspnsubrunlem1  33198  elrgspnsubrunlem2  33199  constrrecl  33759  constrimcl  33760  constrmulcl  33761  constrreinvcl  33762  constrinvcl  33763  constrresqrtcl  33767  constrabscl  33768  constrsqrtcl  33769  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  cos9thpiminply  33778  cos9thpinconstrlem1  33779  oddpwdc  34345  ballotlemfval0  34487  fsum2dsub  34598  breprexplemc  34623  breprexp  34624  circlemeth  34631  fwddifnp1  36153  knoppcnlem6  36486  knoppcnlem9  36489  knoppcn  36492  knoppndvlem2  36501  knoppndvlem4  36503  knoppf  36523  itg2addnclem2  37666  lcmineqlem4  42020  lcmineqlem18  42034  aks4d1p1p2  42058  aks4d1p3  42066  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8  42075  aks4d1p9  42076  posbezout  42088  primrootspoweq0  42094  aks6d1c1  42104  aks6d1c2lem4  42115  aks6d1c2  42118  aks6d1c5lem1  42124  aks6d1c5lem2  42126  2np3bcnp1  42132  sticksstones12a  42145  sticksstones22  42156  aks6d1c6lem3  42160  aks6d1c6lem4  42161  aks6d1c6isolem1  42162  aks6d1c6lem5  42165  bcled  42166  bcle2d  42167  aks6d1c7lem1  42168  aks6d1c7lem2  42169  psrbagres  42534  evlsvvvallem  42549  selvvvval  42573  evlselvlem  42574  evlselv  42575  mhphf  42585  fltnltalem  42650  rmynn  42945  jm2.24nn  42948  jm2.17c  42951  jm2.24  42952  acongrep  42969  acongeq  42972  jm2.18  42977  jm2.23  42985  jm2.20nn  42986  jm2.27a  42994  jm2.27c  42996  rmydioph  43003  hashnzfz  44309  bccbc  44334  binomcxplemnn0  44338  binomcxplemrat  44339  binomcxplemnotnn0  44345  mccllem  45595  expfac  45655  0cnv  45740  lmbr3v  45743  sinaover2ne0  45866  dvnmul  45941  dvnprodlem1  45944  dvnprodlem2  45945  stoweidlem11  46009  stoweidlem26  46024  stoweidlem34  46032  stirlinglem5  46076  fourierdlem11  46116  fourierdlem12  46117  fourierdlem14  46119  fourierdlem15  46120  fourierdlem24  46129  fourierdlem25  46130  fourierdlem36  46141  fourierdlem37  46142  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem64  46168  fourierdlem69  46173  fourierdlem73  46177  fourierdlem79  46183  fourierdlem81  46185  fourierdlem92  46196  fourierdlem93  46197  fourierdlem111  46215  elaa2lem  46231  etransclem3  46235  etransclem7  46239  etransclem10  46242  etransclem24  46256  etransclem27  46259  etransclem35  46267  etransclem44  46276  etransclem46  46278  etransclem47  46279  etransclem48  46280  natglobalincr  46875  2ffzoeq  47328  iccpartigtl  47424  iccpartltu  47426  iccpartgt  47428  0even  48225  2zrngamgm  48233  altgsumbcALT  48341  expnegico01  48507  dig0  48595  nn0sumshdiglem2  48611