Theorem 0zd 11994

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

Syntax hints:   → wi 4   ∈ wcel 2114  0cc0 10537  ℤcz 11982

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-1cn 10595  ax-addrcl 10598  ax-rnegex 10608  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159  df-neg 10873  df-z 11983

This theorem is referenced by:  fzctr  13020  fzosubel3  13099  bcval5  13679  snopiswrd  13871  wrdsymb0  13901  ccatsymb  13936  swrdspsleq  14027  pfxnd  14049  pfxccatin12lem1  14090  swrdccat  14097  repswswrd  14146  eqwrds3  14325  fzomaxdiflem  14702  fsumzcl  15092  isumnn0nn  15197  climcndslem1  15204  climcnds  15206  harmonic  15214  geolim  15226  geolim2  15227  geoisum  15233  geoisumr  15234  mertenslem1  15240  mertenslem2  15241  mertens  15242  risefacval2  15364  fallfacval2  15365  binomfallfaclem2  15394  bpolydiflem  15408  eff  15435  efcvg  15438  reefcl  15440  efcj  15445  eftlub  15462  effsumlt  15464  eflegeo  15474  eirrlem  15557  ruclem6  15588  dvdsmodexp  15615  dvdsmod  15678  pwp1fsum  15742  bitsinv1lem  15790  sadcf  15802  sadadd3  15810  smupf  15827  gcdmultipled  15882  alginv  15919  algcvg  15920  algcvga  15923  algfx  15924  eucalgcvga  15930  eucalg  15931  lcmftp  15980  phiprmpw  16113  iserodd  16172  pcpre1  16179  qexpz  16237  prmreclem4  16255  vdwapun  16310  smndex2dnrinv  18080  odf1  18689  ablsimpgfindlem1  19229  srgbinomlem4  19293  evlslem1  20295  cpmadugsumlemF  21484  dvnff  24520  dgrcl  24823  dgrub  24824  dgrlb  24826  elqaalem2  24909  elqaalem3  24910  geolim3  24928  tayl0  24950  dvtaylp  24958  radcnvlem1  25001  radcnvlem3  25003  radcnv0  25004  radcnvlt2  25007  pserulm  25010  psercn2  25011  pserdvlem2  25016  pserdv2  25018  abelthlem4  25022  abelthlem5  25023  abelthlem6  25024  abelthlem7  25026  abelthlem8  25027  abelthlem9  25028  cos02pilt1  25111  cosne0  25114  logtayl  25243  leibpi  25520  leibpisum  25521  log2cnv  25522  log2tlbnd  25523  basellem3  25660  dchrptlem2  25841  bcmono  25853  lgsne0  25911  crctcshwlkn0lem3  27590  pfxlsw2ccat  30626  wrdt2ind  30627  cycpmco2lem7  30774  cyc3conja  30799  archiabllem1b  30821  oddpwdc  31612  ballotlemfval0  31753  fsum2dsub  31878  breprexplemc  31903  breprexp  31904  circlemeth  31911  fwddifnp1  33626  knoppcnlem6  33837  knoppcnlem9  33840  knoppcn  33843  knoppndvlem2  33852  knoppndvlem4  33854  knoppf  33874  itg2addnclem2  34959  fltnltalem  39294  rmynn  39573  jm2.24nn  39576  jm2.17c  39579  jm2.24  39580  acongrep  39597  acongeq  39600  jm2.18  39605  jm2.23  39613  jm2.20nn  39614  jm2.27a  39622  jm2.27c  39624  rmydioph  39631  hashnzfz  40672  bccbc  40697  binomcxplemnn0  40701  binomcxplemrat  40702  binomcxplemnotnn0  40708  mccllem  41898  expfac  41958  0cnv  42043  lmbr3v  42046  sinaover2ne0  42169  dvnmul  42248  dvnprodlem1  42251  dvnprodlem2  42252  stoweidlem11  42316  stoweidlem26  42331  stoweidlem34  42339  stirlinglem5  42383  fourierdlem11  42423  fourierdlem12  42424  fourierdlem14  42426  fourierdlem15  42427  fourierdlem24  42436  fourierdlem25  42437  fourierdlem36  42448  fourierdlem37  42449  fourierdlem41  42453  fourierdlem48  42459  fourierdlem49  42460  fourierdlem50  42461  fourierdlem64  42475  fourierdlem69  42480  fourierdlem73  42484  fourierdlem79  42490  fourierdlem81  42492  fourierdlem92  42503  fourierdlem93  42504  fourierdlem111  42522  elaa2lem  42538  etransclem3  42542  etransclem7  42546  etransclem10  42549  etransclem24  42563  etransclem27  42566  etransclem35  42574  etransclem44  42583  etransclem46  42585  etransclem47  42586  etransclem48  42587  2ffzoeq  43548  iccpartigtl  43603  iccpartltu  43605  iccpartgt  43607  0even  44222  2zrngamgm  44230  altgsumbcALT  44421  expnegico01  44593  dig0  44686  nn0sumshdiglem2  44702