Theorem 0zd 12536

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

Syntax hints:   → wi 4   ∈ wcel 2114  0cc0 11038  ℤcz 12524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-addrcl 11099  ax-rnegex 11109  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-neg 11380  df-z 12525

This theorem is referenced by:  fzctr  13594  fzosubel3  13681  bcval5  14280  snopiswrd  14485  wrdsymb0  14511  ccatsymb  14545  swrdspsleq  14628  pfxnd  14650  pfxccatin12lem1  14690  swrdccat  14697  repswswrd  14746  eqwrds3  14923  fzomaxdiflem  15305  fsumzcl  15697  isumnn0nn  15807  climcndslem1  15814  climcnds  15816  harmonic  15824  geolim  15835  geolim2  15836  geoisum  15842  geoisumr  15843  mertenslem1  15849  mertenslem2  15850  mertens  15851  risefacval2  15975  fallfacval2  15976  binomfallfaclem2  16005  bpolydiflem  16019  eff  16046  efcvg  16050  reefcl  16052  efcj  16057  eftlub  16076  effsumlt  16078  eflegeo  16088  eirrlem  16171  ruclem6  16202  dvdsmodexp  16229  dvdsmod  16298  pwp1fsum  16360  bitsinv1lem  16410  sadcf  16422  sadadd3  16430  smupf  16447  gcdmultipled  16503  alginv  16544  algcvg  16545  algcvga  16548  algfx  16549  eucalgcvga  16555  eucalg  16556  lcmftp  16605  phiprmpw  16746  iserodd  16806  pcpre1  16813  qexpz  16872  prmreclem4  16890  vdwapun  16945  chnpolfz  18599  smndex2dnrinv  18886  odf1  19537  ablsimpgfindlem1  20084  srgbinomlem4  20210  pzriprnglem5  21465  pzriprnglem8  21468  pzriprnglem10  21470  pzriprnglem11  21471  pzriprng1ALT  21476  evlslem1  22060  evlsvvvallem  22069  psdmul  22132  cpmadugsumlemF  22841  dvnff  25890  dgrcl  26198  dgrub  26199  dgrlb  26201  elqaalem2  26286  elqaalem3  26287  geolim3  26305  tayl0  26327  dvtaylp  26335  radcnvlem1  26378  radcnvlem3  26380  radcnv0  26381  radcnvlt2  26384  pserulm  26387  psercn2  26388  pserdvlem2  26393  pserdv2  26395  abelthlem4  26399  abelthlem5  26400  abelthlem6  26401  abelthlem7  26403  abelthlem8  26404  abelthlem9  26405  cos02pilt1  26490  cosne0  26493  logtayl  26624  leibpi  26906  leibpisum  26907  log2cnv  26908  log2tlbnd  26909  basellem3  27046  dchrptlem2  27228  bcmono  27240  lgsne0  27298  crctcshwlkn0lem3  29880  fzo0opth  32876  pfxlsw2ccat  33010  wrdt2ind  33013  gsumzrsum  33126  gsummulgc2  33127  gsumwrd2dccatlem  33138  cycpmco2lem7  33193  cyc3conja  33218  archiabllem1b  33253  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  esplyfval0  33708  esplyfval2  33709  esplympl  33711  esplyfval3  33716  vietadeg1  33722  constrrecl  33913  constrimcl  33914  constrmulcl  33915  constrreinvcl  33916  constrinvcl  33917  constrresqrtcl  33921  constrabscl  33922  constrsqrtcl  33923  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  cos9thpiminply  33932  cos9thpinconstrlem1  33933  oddpwdc  34498  ballotlemfval0  34640  fsum2dsub  34751  breprexplemc  34776  breprexp  34777  circlemeth  34784  fwddifnp1  36347  knoppcnlem6  36758  knoppcnlem9  36761  knoppcn  36764  knoppndvlem2  36773  knoppndvlem4  36775  knoppf  36795  itg2addnclem2  37993  lcmineqlem4  42471  lcmineqlem18  42485  aks4d1p1p2  42509  aks4d1p3  42517  aks4d1p7d1  42521  aks4d1p7  42522  aks4d1p8  42526  aks4d1p9  42527  posbezout  42539  primrootspoweq0  42545  aks6d1c1  42555  aks6d1c2lem4  42566  aks6d1c2  42569  aks6d1c5lem1  42575  aks6d1c5lem2  42577  2np3bcnp1  42583  sticksstones12a  42596  sticksstones22  42607  aks6d1c6lem3  42611  aks6d1c6lem4  42612  aks6d1c6isolem1  42613  aks6d1c6lem5  42616  bcled  42617  bcle2d  42618  aks6d1c7lem1  42619  aks6d1c7lem2  42620  psrbagres  42989  selvvvval  43018  evlselvlem  43019  evlselv  43020  mhphf  43030  fltnltalem  43095  rmynn  43384  jm2.24nn  43387  jm2.17c  43390  jm2.24  43391  acongrep  43408  acongeq  43411  jm2.18  43416  jm2.23  43424  jm2.20nn  43425  jm2.27a  43433  jm2.27c  43435  rmydioph  43442  hashnzfz  44747  bccbc  44772  binomcxplemnn0  44776  binomcxplemrat  44777  binomcxplemnotnn0  44783  mccllem  46027  expfac  46085  0cnv  46170  lmbr3v  46173  sinaover2ne0  46296  dvnmul  46371  dvnprodlem1  46374  dvnprodlem2  46375  stoweidlem11  46439  stoweidlem26  46454  stoweidlem34  46462  stirlinglem5  46506  fourierdlem11  46546  fourierdlem12  46547  fourierdlem14  46549  fourierdlem15  46550  fourierdlem24  46559  fourierdlem25  46560  fourierdlem36  46571  fourierdlem37  46572  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem64  46598  fourierdlem69  46603  fourierdlem73  46607  fourierdlem79  46613  fourierdlem81  46615  fourierdlem92  46626  fourierdlem93  46627  fourierdlem111  46645  elaa2lem  46661  etransclem3  46665  etransclem7  46669  etransclem10  46672  etransclem24  46686  etransclem27  46689  etransclem35  46697  etransclem44  46706  etransclem46  46708  etransclem47  46709  etransclem48  46710  natglobalincr  47307  chnsubseqwl  47309  chnsubseq  47310  2ffzoeq  47776  iccpartigtl  47883  iccpartltu  47885  iccpartgt  47887  0even  48713  2zrngamgm  48721  altgsumbcALT  48829  expnegico01  48994  dig0  49082  nn0sumshdiglem2  49098