Theorem 0zd 12534

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

Syntax hints:   → wi 4   ∈ wcel 2119  0cc0 11036  ℤcz 12522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-1cn 11094  ax-addrcl 11097  ax-rnegex 11107  ax-cnre 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-neg 11378  df-z 12523

This theorem is referenced by:  fzctr  13592  fzosubel3  13679  bcval5  14278  snopiswrd  14483  wrdsymb0  14509  ccatsymb  14543  swrdspsleq  14626  pfxnd  14648  pfxccatin12lem1  14688  swrdccat  14695  repswswrd  14744  eqwrds3  14921  fzomaxdiflem  15303  fsumzcl  15695  isumnn0nn  15805  climcndslem1  15812  climcnds  15814  harmonic  15822  geolim  15833  geolim2  15834  geoisum  15840  geoisumr  15841  mertenslem1  15847  mertenslem2  15848  mertens  15849  risefacval2  15973  fallfacval2  15974  binomfallfaclem2  16003  bpolydiflem  16017  eff  16044  efcvg  16048  reefcl  16050  efcj  16055  eftlub  16074  effsumlt  16076  eflegeo  16086  eirrlem  16169  ruclem6  16200  dvdsmodexp  16227  dvdsmod  16296  pwp1fsum  16358  bitsinv1lem  16408  sadcf  16420  sadadd3  16428  smupf  16445  gcdmultipled  16501  alginv  16542  algcvg  16543  algcvga  16546  algfx  16547  eucalgcvga  16553  eucalg  16554  lcmftp  16603  phiprmpw  16744  iserodd  16804  pcpre1  16811  qexpz  16870  prmreclem4  16888  vdwapun  16943  chnpolfz  18597  smndex2dnrinv  18884  odf1  19535  ablsimpgfindlem1  20082  srgbinomlem4  20208  pzriprnglem5  21467  pzriprnglem8  21470  pzriprnglem10  21472  pzriprnglem11  21473  pzriprng1ALT  21478  psrbagres  21912  evlslem1  22065  evlsvvvallem  22074  selvvvval  22125  psdmul  22161  cpmadugsumlemF  22866  dvnff  25915  dgrcl  26223  dgrub  26224  dgrlb  26226  elqaalem2  26311  elqaalem3  26312  geolim3  26330  tayl0  26352  dvtaylp  26360  radcnvlem1  26403  radcnvlem3  26405  radcnv0  26406  radcnvlt2  26409  pserulm  26412  psercn2  26413  pserdvlem2  26418  pserdv2  26420  abelthlem4  26424  abelthlem5  26425  abelthlem6  26426  abelthlem7  26428  abelthlem8  26429  abelthlem9  26430  cos02pilt1  26515  cosne0  26518  logtayl  26649  leibpi  26931  leibpisum  26932  log2cnv  26933  log2tlbnd  26934  basellem3  27071  dchrptlem2  27253  bcmono  27265  lgsne0  27323  crctcshwlkn0lem3  29905  fzo0opth  32902  pfxlsw2ccat  33036  wrdt2ind  33039  gsumzrsum  33153  gsummulgc2  33154  gsumwrd2dccatlem  33165  cycpmco2lem7  33220  cyc3conja  33245  archiabllem1b  33280  elrgspnlem1  33330  elrgspnlem2  33331  elrgspnlem3  33332  elrgspnlem4  33333  elrgspnsubrunlem1  33335  elrgspnsubrunlem2  33336  selvply1rhmlemb  33710  esplyfval0  33755  esplyfval2  33756  esplympl  33758  esplyfval3  33763  vietadeg1  33769  constrrecl  33960  constrimcl  33961  constrmulcl  33962  constrreinvcl  33963  constrinvcl  33964  constrresqrtcl  33968  constrabscl  33969  constrsqrtcl  33970  cos9thpiminplylem1  33973  cos9thpiminplylem2  33974  cos9thpiminply  33979  cos9thpinconstrlem1  33980  oddpwdc  34545  ballotlemfval0  34687  fsum2dsub  34798  breprexplemc  34823  breprexp  34824  circlemeth  34831  fwddifnp1  36400  knoppcnlem6  36811  knoppcnlem9  36814  knoppcn  36817  knoppndvlem2  36826  knoppndvlem4  36828  knoppf  36848  itg2addnclem2  38046  lcmineqlem4  42524  lcmineqlem18  42538  aks4d1p1p2  42562  aks4d1p3  42570  aks4d1p7d1  42574  aks4d1p7  42575  aks4d1p8  42579  aks4d1p9  42580  posbezout  42592  primrootspoweq0  42598  aks6d1c1  42608  aks6d1c2lem4  42619  aks6d1c2  42622  aks6d1c5lem1  42628  aks6d1c5lem2  42630  2np3bcnp1  42636  sticksstones12a  42649  sticksstones22  42660  aks6d1c6lem3  42664  aks6d1c6lem4  42665  aks6d1c6isolem1  42666  aks6d1c6lem5  42669  bcled  42670  bcle2d  42671  aks6d1c7lem1  42672  aks6d1c7lem2  42673  evlselvlem  43045  evlselv  43046  mhphf  43054  fltnltalem  43119  rmynn  43408  jm2.24nn  43411  jm2.17c  43414  jm2.24  43415  acongrep  43432  acongeq  43435  jm2.18  43440  jm2.23  43448  jm2.20nn  43449  jm2.27a  43457  jm2.27c  43459  rmydioph  43466  hashnzfz  44771  bccbc  44796  binomcxplemnn0  44800  binomcxplemrat  44801  binomcxplemnotnn0  44807  mccllem  46049  expfac  46107  0cnv  46192  lmbr3v  46195  sinaover2ne0  46318  dvnmul  46393  dvnprodlem1  46396  dvnprodlem2  46397  stoweidlem11  46461  stoweidlem26  46476  stoweidlem34  46484  stirlinglem5  46528  fourierdlem11  46568  fourierdlem12  46569  fourierdlem14  46571  fourierdlem15  46572  fourierdlem24  46581  fourierdlem25  46582  fourierdlem36  46593  fourierdlem37  46594  fourierdlem41  46598  fourierdlem48  46604  fourierdlem49  46605  fourierdlem50  46606  fourierdlem64  46620  fourierdlem69  46625  fourierdlem73  46629  fourierdlem79  46635  fourierdlem81  46637  fourierdlem92  46648  fourierdlem93  46649  fourierdlem111  46667  elaa2lem  46683  etransclem3  46687  etransclem7  46691  etransclem10  46694  etransclem24  46708  etransclem27  46711  etransclem35  46719  etransclem44  46728  etransclem46  46730  etransclem47  46731  etransclem48  46732  natglobalincr  47329  chnsubseqwl  47331  chnsubseq  47332  2ffzoeq  47798  iccpartigtl  47905  iccpartltu  47907  iccpartgt  47909  0even  48735  2zrngamgm  48743  altgsumbcALT  48851  expnegico01  49016  dig0  49104  nn0sumshdiglem2  49120