Theorem 0zd 12500

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

Syntax hints:   → wi 4   ∈ wcel 2113  0cc0 11026  ℤcz 12488

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 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-addrcl 11087  ax-rnegex 11097  ax-cnre 11099

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 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-neg 11367  df-z 12489

This theorem is referenced by:  fzctr  13556  fzosubel3  13642  bcval5  14241  snopiswrd  14446  wrdsymb0  14472  ccatsymb  14506  swrdspsleq  14589  pfxnd  14611  pfxccatin12lem1  14651  swrdccat  14658  repswswrd  14707  eqwrds3  14884  fzomaxdiflem  15266  fsumzcl  15658  isumnn0nn  15765  climcndslem1  15772  climcnds  15774  harmonic  15782  geolim  15793  geolim2  15794  geoisum  15800  geoisumr  15801  mertenslem1  15807  mertenslem2  15808  mertens  15809  risefacval2  15933  fallfacval2  15934  binomfallfaclem2  15963  bpolydiflem  15977  eff  16004  efcvg  16008  reefcl  16010  efcj  16015  eftlub  16034  effsumlt  16036  eflegeo  16046  eirrlem  16129  ruclem6  16160  dvdsmodexp  16187  dvdsmod  16256  pwp1fsum  16318  bitsinv1lem  16368  sadcf  16380  sadadd3  16388  smupf  16405  gcdmultipled  16461  alginv  16502  algcvg  16503  algcvga  16506  algfx  16507  eucalgcvga  16513  eucalg  16514  lcmftp  16563  phiprmpw  16703  iserodd  16763  pcpre1  16770  qexpz  16829  prmreclem4  16847  vdwapun  16902  chnpolfz  18556  smndex2dnrinv  18840  odf1  19491  ablsimpgfindlem1  20038  srgbinomlem4  20164  pzriprnglem5  21440  pzriprnglem8  21443  pzriprnglem10  21445  pzriprnglem11  21446  pzriprng1ALT  21451  evlslem1  22037  evlsvvvallem  22046  psdmul  22109  cpmadugsumlemF  22820  dvnff  25881  dgrcl  26194  dgrub  26195  dgrlb  26197  elqaalem2  26284  elqaalem3  26285  geolim3  26303  tayl0  26325  dvtaylp  26334  radcnvlem1  26378  radcnvlem3  26380  radcnv0  26381  radcnvlt2  26384  pserulm  26387  psercn2  26388  psercn2OLD  26389  pserdvlem2  26394  pserdv2  26396  abelthlem4  26400  abelthlem5  26401  abelthlem6  26402  abelthlem7  26404  abelthlem8  26405  abelthlem9  26406  cos02pilt1  26491  cosne0  26494  logtayl  26625  leibpi  26908  leibpisum  26909  log2cnv  26910  log2tlbnd  26911  basellem3  27049  dchrptlem2  27232  bcmono  27244  lgsne0  27302  crctcshwlkn0lem3  29885  fzo0opth  32883  pfxlsw2ccat  33032  wrdt2ind  33035  gsumzrsum  33148  gsummulgc2  33149  gsumwrd2dccatlem  33159  cycpmco2lem7  33214  cyc3conja  33239  archiabllem1b  33274  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem3  33326  elrgspnlem4  33327  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  esplyfval0  33722  esplyfval2  33723  esplympl  33725  esplyfval3  33730  vietadeg1  33734  constrrecl  33926  constrimcl  33927  constrmulcl  33928  constrreinvcl  33929  constrinvcl  33930  constrresqrtcl  33934  constrabscl  33935  constrsqrtcl  33936  cos9thpiminplylem1  33939  cos9thpiminplylem2  33940  cos9thpiminply  33945  cos9thpinconstrlem1  33946  oddpwdc  34511  ballotlemfval0  34653  fsum2dsub  34764  breprexplemc  34789  breprexp  34790  circlemeth  34797  fwddifnp1  36359  knoppcnlem6  36698  knoppcnlem9  36701  knoppcn  36704  knoppndvlem2  36713  knoppndvlem4  36715  knoppf  36735  itg2addnclem2  37873  lcmineqlem4  42286  lcmineqlem18  42300  aks4d1p1p2  42324  aks4d1p3  42332  aks4d1p7d1  42336  aks4d1p7  42337  aks4d1p8  42341  aks4d1p9  42342  posbezout  42354  primrootspoweq0  42360  aks6d1c1  42370  aks6d1c2lem4  42381  aks6d1c2  42384  aks6d1c5lem1  42390  aks6d1c5lem2  42392  2np3bcnp1  42398  sticksstones12a  42411  sticksstones22  42422  aks6d1c6lem3  42426  aks6d1c6lem4  42427  aks6d1c6isolem1  42428  aks6d1c6lem5  42431  bcled  42432  bcle2d  42433  aks6d1c7lem1  42434  aks6d1c7lem2  42435  psrbagres  42799  selvvvval  42828  evlselvlem  42829  evlselv  42830  mhphf  42840  fltnltalem  42905  rmynn  43198  jm2.24nn  43201  jm2.17c  43204  jm2.24  43205  acongrep  43222  acongeq  43225  jm2.18  43230  jm2.23  43238  jm2.20nn  43239  jm2.27a  43247  jm2.27c  43249  rmydioph  43256  hashnzfz  44561  bccbc  44586  binomcxplemnn0  44590  binomcxplemrat  44591  binomcxplemnotnn0  44597  mccllem  45843  expfac  45901  0cnv  45986  lmbr3v  45989  sinaover2ne0  46112  dvnmul  46187  dvnprodlem1  46190  dvnprodlem2  46191  stoweidlem11  46255  stoweidlem26  46270  stoweidlem34  46278  stirlinglem5  46322  fourierdlem11  46362  fourierdlem12  46363  fourierdlem14  46365  fourierdlem15  46366  fourierdlem24  46375  fourierdlem25  46376  fourierdlem36  46387  fourierdlem37  46388  fourierdlem41  46392  fourierdlem48  46398  fourierdlem49  46399  fourierdlem50  46400  fourierdlem64  46414  fourierdlem69  46419  fourierdlem73  46423  fourierdlem79  46429  fourierdlem81  46431  fourierdlem92  46442  fourierdlem93  46443  fourierdlem111  46461  elaa2lem  46477  etransclem3  46481  etransclem7  46485  etransclem10  46488  etransclem24  46502  etransclem27  46505  etransclem35  46513  etransclem44  46522  etransclem46  46524  etransclem47  46525  etransclem48  46526  natglobalincr  47121  chnsubseqwl  47123  chnsubseq  47124  2ffzoeq  47573  iccpartigtl  47669  iccpartltu  47671  iccpartgt  47673  0even  48483  2zrngamgm  48491  altgsumbcALT  48599  expnegico01  48764  dig0  48852  nn0sumshdiglem2  48868