Theorem 0zd 12601

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

Syntax hints:   → wi 4   ∈ wcel 2099  0cc0 11139  ℤcz 12589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-1cn 11197  ax-addrcl 11200  ax-rnegex 11210  ax-cnre 11212

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rex 3068  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423  df-neg 11478  df-z 12590

This theorem is referenced by:  fzctr  13646  fzosubel3  13726  bcval5  14310  snopiswrd  14506  wrdsymb0  14532  ccatsymb  14565  swrdspsleq  14648  pfxnd  14670  pfxccatin12lem1  14711  swrdccat  14718  repswswrd  14767  eqwrds3  14945  fzomaxdiflem  15322  fsumzcl  15714  isumnn0nn  15821  climcndslem1  15828  climcnds  15830  harmonic  15838  geolim  15849  geolim2  15850  geoisum  15856  geoisumr  15857  mertenslem1  15863  mertenslem2  15864  mertens  15865  risefacval2  15987  fallfacval2  15988  binomfallfaclem2  16017  bpolydiflem  16031  eff  16058  efcvg  16062  reefcl  16064  efcj  16069  eftlub  16086  effsumlt  16088  eflegeo  16098  eirrlem  16181  ruclem6  16212  dvdsmodexp  16239  dvdsmod  16306  pwp1fsum  16368  bitsinv1lem  16416  sadcf  16428  sadadd3  16436  smupf  16453  gcdmultipled  16510  alginv  16546  algcvg  16547  algcvga  16550  algfx  16551  eucalgcvga  16557  eucalg  16558  lcmftp  16607  phiprmpw  16745  iserodd  16804  pcpre1  16811  qexpz  16870  prmreclem4  16888  vdwapun  16943  smndex2dnrinv  18867  odf1  19517  ablsimpgfindlem1  20064  srgbinomlem4  20169  pzriprnglem5  21411  pzriprnglem8  21414  pzriprnglem10  21416  pzriprnglem11  21417  pzriprng1ALT  21422  evlslem1  22028  psdmul  22090  cpmadugsumlemF  22791  dvnff  25866  dgrcl  26180  dgrub  26181  dgrlb  26183  elqaalem2  26268  elqaalem3  26269  geolim3  26287  tayl0  26309  dvtaylp  26318  radcnvlem1  26362  radcnvlem3  26364  radcnv0  26365  radcnvlt2  26368  pserulm  26371  psercn2  26372  psercn2OLD  26373  pserdvlem2  26378  pserdv2  26380  abelthlem4  26384  abelthlem5  26385  abelthlem6  26386  abelthlem7  26388  abelthlem8  26389  abelthlem9  26390  cos02pilt1  26473  cosne0  26476  logtayl  26607  leibpi  26887  leibpisum  26888  log2cnv  26889  log2tlbnd  26890  basellem3  27028  dchrptlem2  27211  bcmono  27223  lgsne0  27281  crctcshwlkn0lem3  29636  pfxlsw2ccat  32686  wrdt2ind  32687  cycpmco2lem7  32866  cyc3conja  32891  archiabllem1b  32913  oddpwdc  33974  ballotlemfval0  34115  fsum2dsub  34239  breprexplemc  34264  breprexp  34265  circlemeth  34272  fwddifnp1  35761  knoppcnlem6  35973  knoppcnlem9  35976  knoppcn  35979  knoppndvlem2  35988  knoppndvlem4  35990  knoppf  36010  itg2addnclem2  37145  lcmineqlem4  41503  lcmineqlem18  41517  aks4d1p1p2  41541  aks4d1p3  41549  aks4d1p7d1  41553  aks4d1p7  41554  aks4d1p8  41558  aks4d1p9  41559  posbezout  41571  primrootspoweq0  41577  aks6d1c1  41587  aks6d1c2lem4  41598  aks6d1c2  41601  aks6d1c5lem1  41607  aks6d1c5lem2  41609  2np3bcnp1  41616  sticksstones12a  41629  sticksstones22  41640  aks6d1c6lem3  41644  aks6d1c6lem4  41645  aks6d1c6isolem1  41646  aks6d1c6lem5  41649  bcled  41650  bcle2d  41651  aks6d1c7lem1  41652  aks6d1c7lem2  41653  metakunt29  41685  metakunt30  41686  metakunt32  41688  metakunt33  41689  psrbagres  41776  evlsvvvallem  41794  selvvvval  41818  evlselvlem  41819  evlselv  41820  mhphf  41830  fltnltalem  42086  rmynn  42377  jm2.24nn  42380  jm2.17c  42383  jm2.24  42384  acongrep  42401  acongeq  42404  jm2.18  42409  jm2.23  42417  jm2.20nn  42418  jm2.27a  42426  jm2.27c  42428  rmydioph  42435  hashnzfz  43757  bccbc  43782  binomcxplemnn0  43786  binomcxplemrat  43787  binomcxplemnotnn0  43793  mccllem  44985  expfac  45045  0cnv  45130  lmbr3v  45133  sinaover2ne0  45256  dvnmul  45331  dvnprodlem1  45334  dvnprodlem2  45335  stoweidlem11  45399  stoweidlem26  45414  stoweidlem34  45422  stirlinglem5  45466  fourierdlem11  45506  fourierdlem12  45507  fourierdlem14  45509  fourierdlem15  45510  fourierdlem24  45519  fourierdlem25  45520  fourierdlem36  45531  fourierdlem37  45532  fourierdlem41  45536  fourierdlem48  45542  fourierdlem49  45543  fourierdlem50  45544  fourierdlem64  45558  fourierdlem69  45563  fourierdlem73  45567  fourierdlem79  45573  fourierdlem81  45575  fourierdlem92  45586  fourierdlem93  45587  fourierdlem111  45605  elaa2lem  45621  etransclem3  45625  etransclem7  45629  etransclem10  45632  etransclem24  45646  etransclem27  45649  etransclem35  45657  etransclem44  45666  etransclem46  45668  etransclem47  45669  etransclem48  45670  natglobalincr  46263  2ffzoeq  46708  iccpartigtl  46763  iccpartltu  46765  iccpartgt  46767  0even  47299  2zrngamgm  47307  altgsumbcALT  47417  expnegico01  47586  dig0  47679  nn0sumshdiglem2  47695