Theorem 0zd 12574

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

Syntax hints:   → wi 4   ∈ wcel 2141  0cc0 11067  ℤcz 12562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-1cn 11125  ax-addrcl 11128  ax-rnegex 11138  ax-cnre 11140

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6472  df-fv 6524  df-ov 7394  df-neg 11411  df-z 12563

This theorem is referenced by:  fzctr  13639  fzosubel3  13726  bcval5  14325  snopiswrd  14530  wrdsymb0  14556  ccatsymb  14590  swrdspsleq  14673  pfxnd  14695  pfxccatin12lem1  14735  swrdccat  14742  repswswrd  14791  eqwrds3  14968  fzomaxdiflem  15361  fsumzcl  15753  isumnn0nn  15863  climcndslem1  15870  climcnds  15872  harmonic  15880  geolim  15891  geolim2  15892  geoisum  15898  geoisumr  15899  mertenslem1  15905  mertenslem2  15906  mertens  15907  risefacval2  16031  fallfacval2  16032  binomfallfaclem2  16061  bpolydiflem  16075  eff  16102  efcvg  16106  reefcl  16108  efcj  16113  eftlub  16132  effsumlt  16134  eflegeo  16144  eirrlem  16227  ruclem6  16258  dvdsmodexp  16285  dvdsmod  16354  pwp1fsum  16416  bitsinv1lem  16466  sadcf  16478  sadadd3  16486  smupf  16503  gcdmultipled  16559  alginv  16600  algcvg  16601  algcvga  16604  algfx  16605  eucalgcvga  16611  eucalg  16612  lcmftp  16661  phiprmpw  16802  iserodd  16862  pcpre1  16869  qexpz  16928  prmreclem4  16946  vdwapun  17001  chnpolfz  18656  smndex2dnrinv  18943  odf1  19593  ablsimpgfindlem1  20140  srgbinomlem4  20266  pzriprnglem5  21525  pzriprnglem8  21528  pzriprnglem10  21530  pzriprnglem11  21531  pzriprng1ALT  21536  psrbagres  21970  evlslem1  22123  evlsvvvallem  22132  selvvvval  22183  psdmul  22219  cpmadugsumlemF  22924  dvnff  25973  dgrcl  26281  dgrub  26282  dgrlb  26284  elqaalem2  26372  elqaalem3  26373  geolim3  26391  tayl0  26413  dvtaylp  26421  radcnvlem1  26464  radcnvlem3  26466  radcnv0  26467  radcnvlt2  26470  pserulm  26473  psercn2  26474  pserdvlem2  26479  pserdv2  26481  abelthlem4  26485  abelthlem5  26486  abelthlem6  26487  abelthlem7  26489  abelthlem8  26490  abelthlem9  26491  cos02pilt1  26579  cosne0  26582  logtayl  26713  leibpi  26995  leibpisum  26996  log2cnv  26997  log2tlbnd  26998  basellem3  27135  dchrptlem2  27317  bcmono  27329  lgsne0  27387  crctcshwlkn0lem3  29969  fzo0opth  32966  pfxlsw2ccat  33089  wrdt2ind  33092  gsumzrsum  33206  gsummulgc2  33207  gsumwrd2dccatlem  33218  cycpmco2lem7  33273  cyc3conja  33298  archiabllem1b  33333  elrgspnlem1  33384  elrgspnlem2  33385  elrgspnlem3  33386  elrgspnlem4  33387  elrgspnsubrunlem1  33389  elrgspnsubrunlem2  33390  selvply1rhmlemb  33777  esplyfval0  33822  esplyfval2  33823  esplympl  33825  esplyfval3  33830  vietadeg1  33836  constrrecl  34027  constrimcl  34028  constrmulcl  34029  constrreinvcl  34030  constrinvcl  34031  constrresqrtcl  34035  constrabscl  34036  constrsqrtcl  34037  cos9thpiminplylem1  34040  cos9thpiminplylem2  34041  cos9thpiminply  34046  cos9thpinconstrlem1  34047  oddpwdc  34612  ballotlemfval0  34754  fsum2dsub  34862  breprexplemc  34887  breprexp  34888  circlemeth  34895  fwddifnp1  36476  knoppcnlem6  36897  knoppcnlem9  36900  knoppcn  36903  knoppndvlem2  36912  knoppndvlem4  36914  knoppf  36934  itg2addnclem2  38132  lcmineqlem4  42610  lcmineqlem18  42624  aks4d1p1p2  42648  aks4d1p3  42656  aks4d1p7d1  42660  aks4d1p7  42661  aks4d1p8  42665  aks4d1p9  42666  posbezout  42678  primrootspoweq0  42684  aks6d1c1  42694  aks6d1c2lem4  42705  aks6d1c2  42708  aks6d1c5lem1  42714  aks6d1c5lem2  42716  2np3bcnp1  42722  sticksstones12a  42735  sticksstones22  42746  aks6d1c6lem3  42750  aks6d1c6lem4  42751  aks6d1c6isolem1  42752  aks6d1c6lem5  42755  bcled  42756  bcle2d  42757  aks6d1c7lem1  42758  aks6d1c7lem2  42759  evlselvlem  43131  evlselv  43132  mhphf  43140  fltnltalem  43205  rmynn  43494  jm2.24nn  43497  jm2.17c  43500  jm2.24  43501  acongrep  43518  acongeq  43521  jm2.18  43526  jm2.23  43534  jm2.20nn  43535  jm2.27a  43543  jm2.27c  43545  rmydioph  43552  hashnzfz  44857  bccbc  44882  binomcxplemnn0  44886  binomcxplemrat  44887  binomcxplemnotnn0  44893  mccllem  46134  expfac  46192  0cnv  46277  lmbr3v  46280  sinaover2ne0  46403  dvnmul  46478  dvnprodlem1  46481  dvnprodlem2  46482  stoweidlem11  46546  stoweidlem26  46561  stoweidlem34  46569  stirlinglem5  46613  fourierdlem11  46653  fourierdlem12  46654  fourierdlem14  46656  fourierdlem15  46657  fourierdlem24  46666  fourierdlem25  46667  fourierdlem36  46678  fourierdlem37  46679  fourierdlem41  46683  fourierdlem48  46689  fourierdlem49  46690  fourierdlem50  46691  fourierdlem64  46705  fourierdlem69  46710  fourierdlem73  46714  fourierdlem79  46720  fourierdlem81  46722  fourierdlem92  46733  fourierdlem93  46734  fourierdlem111  46752  elaa2lem  46768  etransclem3  46772  etransclem7  46776  etransclem10  46779  etransclem24  46793  etransclem27  46796  etransclem35  46804  etransclem44  46813  etransclem46  46815  etransclem47  46816  etransclem48  46817  natglobalincr  47414  chnsubseqwl  47416  chnsubseq  47417  2ffzoeq  47883  iccpartigtl  47990  iccpartltu  47992  iccpartgt  47994  0even  48820  2zrngamgm  48828  altgsumbcALT  48936  expnegico01  49101  dig0  49189  nn0sumshdiglem2  49205