Theorem 0zd 12698

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  0cc0 11193  ℤcz 12686

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11251  ax-addrcl 11254  ax-rnegex 11264  ax-cnre 11266

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-ov 7421  df-neg 11537  df-z 12687

This theorem is used by:  fzctr  13767  fzosubel3  13854  bcval5  14455  snopiswrd  14661  wrdsymb0  14687  ccatsymb  14721  swrdspsleq  14808  pfxnd  14830  pfxccatin12lem1  14870  swrdccat  14877  repswswrd  14928  eqwrds3  15107  fzomaxdiflem  15503  fsumzcl  15894  isumnn0nn  16004  climcndslem1  16011  climcnds  16013  harmonic  16021  geolim  16032  geolim2  16033  geoisum  16039  geoisumr  16040  mertenslem1  16046  mertenslem2  16047  mertens  16048  risefacval2  16170  fallfacval2  16171  binomfallfaclem2  16199  bpolydiflem  16213  eff  16240  efcvg  16244  reefcl  16246  efcj  16251  eftlub  16270  effsumlt  16272  eflegeo  16282  eirrlem  16365  ruclem6  16396  dvdsmodexp  16423  dvdsmod  16492  pwp1fsum  16554  bitsinv1lem  16604  sadcf  16616  sadadd3  16624  smupf  16641  gcdmultipled  16700  alginv  16743  algcvg  16744  algcvga  16747  algfx  16748  eucalgcvga  16754  eucalg  16755  lcmftp  16804  phiprmpw  16946  iserodd  17006  pcpre1  17013  qexpz  17072  prmreclem4  17090  vdwapun  17145  chnpolfz  18800  smndex2dnrinv  19107  odf1  19769  ablsimpgfindlem1  20316  srgbinomlem4  20448  pzriprnglem5  21784  pzriprnglem8  21787  pzriprnglem10  21789  pzriprnglem11  21790  pzriprng1ALT  21795  psrbagres  22231  evlslem1  22384  evlsvvvallem  22393  selvvvval  22444  psdmul  22480  cpmadugsumlemF  23187  dvnff  26236  dgrcl  26545  dgrub  26546  dgrlb  26548  elqaalem2  26636  elqaalem3  26637  geolim3  26659  tayl0  26682  dvtaylp  26690  radcnvlem1  26733  radcnvlem3  26735  radcnv0  26736  radcnvlt2  26739  pserulm  26742  psercn2  26743  pserdvlem2  26748  pserdv2  26750  abelthlem4  26754  abelthlem5  26755  abelthlem6  26756  abelthlem7  26758  abelthlem8  26759  abelthlem9  26760  cos02pilt1  26847  cosne0  26850  logtayl  26981  leibpi  27263  leibpisum  27264  log2cnv  27265  log2tlbnd  27266  basellem3  27403  dchrptlem2  27585  bcmono  27597  lgsne0  27655  crctcshwlkn0lem3  30394  fzo0opth  33388  pfxlsw2ccat  33506  wrdt2ind  33509  gsumzrsum  33619  gsummulgc2  33620  gsumwrd2dccatlem  33631  cycpmco2lem7  33686  cyc3conja  33711  archiabllem1b  33746  elrgspnlem1  33796  elrgspnlem2  33797  elrgspnlem3  33798  elrgspnlem4  33799  elrgspnsubrunlem1  33801  elrgspnsubrunlem2  33802  selvply1rhmlemb  34144  esplyfval0  34189  esplyfval2  34190  esplympl  34192  esplyfval3  34197  vietadeg1  34203  constrrecl  34394  constrimcl  34395  constrmulcl  34396  constrreinvcl  34397  constrinvcl  34398  constrresqrtcl  34402  constrabscl  34403  constrsqrtcl  34404  cos9thpiminplylem1  34407  cos9thpiminplylem2  34408  cos9thpiminply  34413  cos9thpinconstrlem1  34414  oddpwdc  34979  ballotlemfval0  35121  fsum2dsub  35229  breprexplemc  35254  breprexp  35255  circlemeth  35262  fwddifnp1  36910  knoppcnlem6  37344  knoppcnlem9  37347  knoppcn  37350  knoppndvlem2  37359  knoppndvlem4  37361  knoppf  37381  itg2addnclem2  38570  lcmineqlem4  43062  lcmineqlem18  43076  aks4d1p1p2  43100  aks4d1p3  43108  aks4d1p7d1  43112  aks4d1p7  43113  aks4d1p8  43117  aks4d1p9  43118  posbezout  43130  primrootspoweq0  43136  aks6d1c1  43146  aks6d1c2lem4  43157  aks6d1c2  43160  aks6d1c5lem1  43166  aks6d1c5lem2  43168  2np3bcnp1  43174  sticksstones12a  43187  sticksstones22  43198  aks6d1c6lem3  43202  aks6d1c6lem4  43203  aks6d1c6isolem1  43204  aks6d1c6lem5  43207  bcled  43208  bcle2d  43209  aks6d1c7lem1  43210  aks6d1c7lem2  43211  evlselvlem  43596  evlselv  43597  mhphf  43605  fltnltalem  43653  rmynn  43942  jm2.24nn  43945  jm2.17c  43948  jm2.24  43949  acongrep  43966  acongeq  43969  jm2.18  43974  jm2.23  43982  jm2.20nn  43983  jm2.27a  43991  jm2.27c  43993  rmydioph  44000  hashnzfz  45289  bccbc  45314  binomcxplemnn0  45318  binomcxplemrat  45319  binomcxplemnotnn0  45325  mccllem  46578  expfac  46636  0cnv  46721  lmbr3v  46724  sinaover2ne0  46847  dvnmul  46922  dvnprodlem1  46925  dvnprodlem2  46926  stoweidlem11  46990  stoweidlem26  47005  stoweidlem34  47013  stirlinglem5  47057  fourierdlem11  47097  fourierdlem12  47098  fourierdlem14  47100  fourierdlem15  47101  fourierdlem24  47110  fourierdlem25  47111  fourierdlem36  47122  fourierdlem37  47123  fourierdlem41  47127  fourierdlem48  47133  fourierdlem49  47134  fourierdlem50  47135  fourierdlem64  47149  fourierdlem69  47154  fourierdlem73  47158  fourierdlem79  47164  fourierdlem81  47166  fourierdlem92  47177  fourierdlem93  47178  fourierdlem111  47196  elaa2lem  47212  etransclem3  47216  etransclem7  47220  etransclem10  47223  etransclem24  47237  etransclem27  47240  etransclem35  47248  etransclem44  47257  etransclem46  47259  etransclem47  47260  etransclem48  47261  chnsubseqwl  47858  chnsubseq  47859  2ffzoeq  48367  iccpartigtl  48474  iccpartltu  48476  iccpartgt  48478  0even  49303  2zrngamgm  49311  altgsumbcALT  49434  expnegico01  49599  dig0  49687  nn0sumshdiglem2  49703