Theorem 0zd 12480

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

Syntax hints:   → wi 4   ∈ wcel 2111  0cc0 11006  ℤcz 12468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11064  ax-addrcl 11067  ax-rnegex 11077  ax-cnre 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-neg 11347  df-z 12469

This theorem is referenced by:  fzctr  13540  fzosubel3  13626  bcval5  14225  snopiswrd  14430  wrdsymb0  14456  ccatsymb  14490  swrdspsleq  14573  pfxnd  14595  pfxccatin12lem1  14635  swrdccat  14642  repswswrd  14691  eqwrds3  14868  fzomaxdiflem  15250  fsumzcl  15642  isumnn0nn  15749  climcndslem1  15756  climcnds  15758  harmonic  15766  geolim  15777  geolim2  15778  geoisum  15784  geoisumr  15785  mertenslem1  15791  mertenslem2  15792  mertens  15793  risefacval2  15917  fallfacval2  15918  binomfallfaclem2  15947  bpolydiflem  15961  eff  15988  efcvg  15992  reefcl  15994  efcj  15999  eftlub  16018  effsumlt  16020  eflegeo  16030  eirrlem  16113  ruclem6  16144  dvdsmodexp  16171  dvdsmod  16240  pwp1fsum  16302  bitsinv1lem  16352  sadcf  16364  sadadd3  16372  smupf  16389  gcdmultipled  16445  alginv  16486  algcvg  16487  algcvga  16490  algfx  16491  eucalgcvga  16497  eucalg  16498  lcmftp  16547  phiprmpw  16687  iserodd  16747  pcpre1  16754  qexpz  16813  prmreclem4  16831  vdwapun  16886  chnpolfz  18539  smndex2dnrinv  18823  odf1  19475  ablsimpgfindlem1  20022  srgbinomlem4  20148  pzriprnglem5  21423  pzriprnglem8  21426  pzriprnglem10  21428  pzriprnglem11  21429  pzriprng1ALT  21434  evlslem1  22018  psdmul  22082  cpmadugsumlemF  22792  dvnff  25853  dgrcl  26166  dgrub  26167  dgrlb  26169  elqaalem2  26256  elqaalem3  26257  geolim3  26275  tayl0  26297  dvtaylp  26306  radcnvlem1  26350  radcnvlem3  26352  radcnv0  26353  radcnvlt2  26356  pserulm  26359  psercn2  26360  psercn2OLD  26361  pserdvlem2  26366  pserdv2  26368  abelthlem4  26372  abelthlem5  26373  abelthlem6  26374  abelthlem7  26376  abelthlem8  26377  abelthlem9  26378  cos02pilt1  26463  cosne0  26466  logtayl  26597  leibpi  26880  leibpisum  26881  log2cnv  26882  log2tlbnd  26883  basellem3  27021  dchrptlem2  27204  bcmono  27216  lgsne0  27274  crctcshwlkn0lem3  29791  fzo0opth  32783  pfxlsw2ccat  32929  wrdt2ind  32932  gsumzrsum  33037  gsummulgc2  33038  gsumwrd2dccatlem  33044  cycpmco2lem7  33099  cyc3conja  33124  archiabllem1b  33159  elrgspnlem1  33207  elrgspnlem2  33208  elrgspnlem3  33209  elrgspnlem4  33210  elrgspnsubrunlem1  33212  elrgspnsubrunlem2  33213  esplympl  33586  constrrecl  33780  constrimcl  33781  constrmulcl  33782  constrreinvcl  33783  constrinvcl  33784  constrresqrtcl  33788  constrabscl  33789  constrsqrtcl  33790  cos9thpiminplylem1  33793  cos9thpiminplylem2  33794  cos9thpiminply  33799  cos9thpinconstrlem1  33800  oddpwdc  34365  ballotlemfval0  34507  fsum2dsub  34618  breprexplemc  34643  breprexp  34644  circlemeth  34651  fwddifnp1  36205  knoppcnlem6  36538  knoppcnlem9  36541  knoppcn  36544  knoppndvlem2  36553  knoppndvlem4  36555  knoppf  36575  itg2addnclem2  37718  lcmineqlem4  42071  lcmineqlem18  42085  aks4d1p1p2  42109  aks4d1p3  42117  aks4d1p7d1  42121  aks4d1p7  42122  aks4d1p8  42126  aks4d1p9  42127  posbezout  42139  primrootspoweq0  42145  aks6d1c1  42155  aks6d1c2lem4  42166  aks6d1c2  42169  aks6d1c5lem1  42175  aks6d1c5lem2  42177  2np3bcnp1  42183  sticksstones12a  42196  sticksstones22  42207  aks6d1c6lem3  42211  aks6d1c6lem4  42212  aks6d1c6isolem1  42213  aks6d1c6lem5  42216  bcled  42217  bcle2d  42218  aks6d1c7lem1  42219  aks6d1c7lem2  42220  psrbagres  42585  evlsvvvallem  42600  selvvvval  42624  evlselvlem  42625  evlselv  42626  mhphf  42636  fltnltalem  42701  rmynn  42995  jm2.24nn  42998  jm2.17c  43001  jm2.24  43002  acongrep  43019  acongeq  43022  jm2.18  43027  jm2.23  43035  jm2.20nn  43036  jm2.27a  43044  jm2.27c  43046  rmydioph  43053  hashnzfz  44359  bccbc  44384  binomcxplemnn0  44388  binomcxplemrat  44389  binomcxplemnotnn0  44395  mccllem  45643  expfac  45701  0cnv  45786  lmbr3v  45789  sinaover2ne0  45912  dvnmul  45987  dvnprodlem1  45990  dvnprodlem2  45991  stoweidlem11  46055  stoweidlem26  46070  stoweidlem34  46078  stirlinglem5  46122  fourierdlem11  46162  fourierdlem12  46163  fourierdlem14  46165  fourierdlem15  46166  fourierdlem24  46175  fourierdlem25  46176  fourierdlem36  46187  fourierdlem37  46188  fourierdlem41  46192  fourierdlem48  46198  fourierdlem49  46199  fourierdlem50  46200  fourierdlem64  46214  fourierdlem69  46219  fourierdlem73  46223  fourierdlem79  46229  fourierdlem81  46231  fourierdlem92  46242  fourierdlem93  46243  fourierdlem111  46261  elaa2lem  46277  etransclem3  46281  etransclem7  46285  etransclem10  46288  etransclem24  46302  etransclem27  46305  etransclem35  46313  etransclem44  46322  etransclem46  46324  etransclem47  46325  etransclem48  46326  natglobalincr  46921  2ffzoeq  47364  iccpartigtl  47460  iccpartltu  47462  iccpartgt  47464  0even  48274  2zrngamgm  48282  altgsumbcALT  48390  expnegico01  48556  dig0  48644  nn0sumshdiglem2  48660