Theorem 0zd 12548

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

Syntax hints:   → wi 4   ∈ wcel 2109  0cc0 11075  ℤcz 12536

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 2702  ax-1cn 11133  ax-addrcl 11136  ax-rnegex 11146  ax-cnre 11148

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 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-neg 11415  df-z 12537

This theorem is referenced by:  fzctr  13608  fzosubel3  13694  bcval5  14290  snopiswrd  14495  wrdsymb0  14521  ccatsymb  14554  swrdspsleq  14637  pfxnd  14659  pfxccatin12lem1  14700  swrdccat  14707  repswswrd  14756  eqwrds3  14934  fzomaxdiflem  15316  fsumzcl  15708  isumnn0nn  15815  climcndslem1  15822  climcnds  15824  harmonic  15832  geolim  15843  geolim2  15844  geoisum  15850  geoisumr  15851  mertenslem1  15857  mertenslem2  15858  mertens  15859  risefacval2  15983  fallfacval2  15984  binomfallfaclem2  16013  bpolydiflem  16027  eff  16054  efcvg  16058  reefcl  16060  efcj  16065  eftlub  16084  effsumlt  16086  eflegeo  16096  eirrlem  16179  ruclem6  16210  dvdsmodexp  16237  dvdsmod  16306  pwp1fsum  16368  bitsinv1lem  16418  sadcf  16430  sadadd3  16438  smupf  16455  gcdmultipled  16511  alginv  16552  algcvg  16553  algcvga  16556  algfx  16557  eucalgcvga  16563  eucalg  16564  lcmftp  16613  phiprmpw  16753  iserodd  16813  pcpre1  16820  qexpz  16879  prmreclem4  16897  vdwapun  16952  smndex2dnrinv  18849  odf1  19499  ablsimpgfindlem1  20046  srgbinomlem4  20145  pzriprnglem5  21402  pzriprnglem8  21405  pzriprnglem10  21407  pzriprnglem11  21408  pzriprng1ALT  21413  evlslem1  21996  psdmul  22060  cpmadugsumlemF  22770  dvnff  25832  dgrcl  26145  dgrub  26146  dgrlb  26148  elqaalem2  26235  elqaalem3  26236  geolim3  26254  tayl0  26276  dvtaylp  26285  radcnvlem1  26329  radcnvlem3  26331  radcnv0  26332  radcnvlt2  26335  pserulm  26338  psercn2  26339  psercn2OLD  26340  pserdvlem2  26345  pserdv2  26347  abelthlem4  26351  abelthlem5  26352  abelthlem6  26353  abelthlem7  26355  abelthlem8  26356  abelthlem9  26357  cos02pilt1  26442  cosne0  26445  logtayl  26576  leibpi  26859  leibpisum  26860  log2cnv  26861  log2tlbnd  26862  basellem3  27000  dchrptlem2  27183  bcmono  27195  lgsne0  27253  crctcshwlkn0lem3  29749  fzo0opth  32735  pfxlsw2ccat  32879  wrdt2ind  32882  gsumzrsum  33006  gsummulgc2  33007  gsumwrd2dccatlem  33013  cycpmco2lem7  33096  cyc3conja  33121  archiabllem1b  33153  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem3  33202  elrgspnlem4  33203  elrgspnsubrunlem1  33205  elrgspnsubrunlem2  33206  constrrecl  33766  constrimcl  33767  constrmulcl  33768  constrreinvcl  33769  constrinvcl  33770  constrresqrtcl  33774  constrabscl  33775  constrsqrtcl  33776  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  cos9thpiminply  33785  cos9thpinconstrlem1  33786  oddpwdc  34352  ballotlemfval0  34494  fsum2dsub  34605  breprexplemc  34630  breprexp  34631  circlemeth  34638  fwddifnp1  36160  knoppcnlem6  36493  knoppcnlem9  36496  knoppcn  36499  knoppndvlem2  36508  knoppndvlem4  36510  knoppf  36530  itg2addnclem2  37673  lcmineqlem4  42027  lcmineqlem18  42041  aks4d1p1p2  42065  aks4d1p3  42073  aks4d1p7d1  42077  aks4d1p7  42078  aks4d1p8  42082  aks4d1p9  42083  posbezout  42095  primrootspoweq0  42101  aks6d1c1  42111  aks6d1c2lem4  42122  aks6d1c2  42125  aks6d1c5lem1  42131  aks6d1c5lem2  42133  2np3bcnp1  42139  sticksstones12a  42152  sticksstones22  42163  aks6d1c6lem3  42167  aks6d1c6lem4  42168  aks6d1c6isolem1  42169  aks6d1c6lem5  42172  bcled  42173  bcle2d  42174  aks6d1c7lem1  42175  aks6d1c7lem2  42176  psrbagres  42541  evlsvvvallem  42556  selvvvval  42580  evlselvlem  42581  evlselv  42582  mhphf  42592  fltnltalem  42657  rmynn  42952  jm2.24nn  42955  jm2.17c  42958  jm2.24  42959  acongrep  42976  acongeq  42979  jm2.18  42984  jm2.23  42992  jm2.20nn  42993  jm2.27a  43001  jm2.27c  43003  rmydioph  43010  hashnzfz  44316  bccbc  44341  binomcxplemnn0  44345  binomcxplemrat  44346  binomcxplemnotnn0  44352  mccllem  45602  expfac  45662  0cnv  45747  lmbr3v  45750  sinaover2ne0  45873  dvnmul  45948  dvnprodlem1  45951  dvnprodlem2  45952  stoweidlem11  46016  stoweidlem26  46031  stoweidlem34  46039  stirlinglem5  46083  fourierdlem11  46123  fourierdlem12  46124  fourierdlem14  46126  fourierdlem15  46127  fourierdlem24  46136  fourierdlem25  46137  fourierdlem36  46148  fourierdlem37  46149  fourierdlem41  46153  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem64  46175  fourierdlem69  46180  fourierdlem73  46184  fourierdlem79  46190  fourierdlem81  46192  fourierdlem92  46203  fourierdlem93  46204  fourierdlem111  46222  elaa2lem  46238  etransclem3  46242  etransclem7  46246  etransclem10  46249  etransclem24  46263  etransclem27  46266  etransclem35  46274  etransclem44  46283  etransclem46  46285  etransclem47  46286  etransclem48  46287  natglobalincr  46882  2ffzoeq  47332  iccpartigtl  47428  iccpartltu  47430  iccpartgt  47432  0even  48229  2zrngamgm  48237  altgsumbcALT  48345  expnegico01  48511  dig0  48599  nn0sumshdiglem2  48615