Theorem 0zd 11389

Description: Zero is an integer, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
0zd	⊢ (𝜑 → 0 ∈ ℤ)

Proof of Theorem 0zd

Step	Hyp	Ref	Expression
1		0z 11388	. 2 ⊢ 0 ∈ ℤ
2	1	a1i 11	1 ⊢ (𝜑 → 0 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 1990  0cc0 9936  ℤcz 11377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-neg 10269  df-z 11378

This theorem is referenced by:  fzctr  12451  fzosubel3  12528  bcval5  13105  snopiswrd  13314  wrdsymb0  13339  ccatsymb  13366  swrdspsleq  13449  swrdccatin12lem2b  13486  swrdccat  13493  repswswrd  13531  eqwrds3  13704  fzomaxdiflem  14082  fsumzcl  14466  isumnn0nn  14574  climcndslem1  14581  climcnds  14583  harmonic  14591  geolim  14601  geolim2  14602  geoisum  14608  geoisumr  14609  mertenslem1  14616  mertenslem2  14617  mertens  14618  risefacval2  14741  fallfacval2  14742  binomfallfaclem2  14771  bpolydiflem  14785  eff  14812  efcvg  14815  reefcl  14817  efcj  14822  eftlub  14839  effsumlt  14841  eflegeo  14851  eirrlem  14932  ruclem6  14964  dvdsmod  15050  pwp1fsum  15114  bitsinv1lem  15163  sadcf  15175  sadadd3  15183  smupf  15200  alginv  15288  algcvg  15289  algcvga  15292  algfx  15293  eucalgcvga  15299  eucalg  15300  lcmftp  15349  phiprmpw  15481  fermltl  15489  iserodd  15540  pcpre1  15547  qexpz  15605  prmreclem4  15623  vdwapun  15678  odf1  17979  srgbinomlem4  18543  evlslem1  19515  cpmadugsumlemF  20681  dvnff  23686  dgrcl  23989  dgrub  23990  dgrlb  23992  elqaalem2  24075  elqaalem3  24076  geolim3  24094  tayl0  24116  dvtaylp  24124  radcnvlem1  24167  radcnvlem3  24169  radcnv0  24170  radcnvlt2  24173  pserulm  24176  psercn2  24177  pserdvlem2  24182  pserdv2  24184  abelthlem4  24188  abelthlem5  24189  abelthlem6  24190  abelthlem7  24192  abelthlem8  24193  abelthlem9  24194  cosne0  24276  logtayl  24406  leibpi  24669  leibpisum  24670  log2cnv  24671  log2tlbnd  24672  basellem3  24809  dchrptlem2  24990  bcmono  25002  lgslem4  25025  lgsne0  25060  crctcshwlkn0lem3  26704  wwlksnextproplem1  26804  archiabllem1b  29746  oddpwdc  30416  ballotlemfval0  30557  fsum2dsub  30685  breprexplemc  30710  breprexp  30711  circlemeth  30718  fwddifnp1  32272  knoppcnlem6  32488  knoppcnlem9  32491  knoppcn  32494  knoppndvlem2  32504  knoppndvlem4  32506  knoppf  32526  itg2addnclem2  33462  rmynn  37523  jm2.24nn  37526  jm2.17c  37529  jm2.24  37530  acongrep  37547  acongeq  37550  jm2.18  37555  jm2.23  37563  jm2.20nn  37564  jm2.27a  37572  jm2.27c  37574  rmydioph  37581  hashnzfz  38519  bccbc  38544  binomcxplemnn0  38548  binomcxplemrat  38549  binomcxplemnotnn0  38555  mccllem  39829  expfac  39889  0cnv  39974  lmbr3v  39977  sinaover2ne0  40079  dvnmul  40158  dvnprodlem1  40161  dvnprodlem2  40162  stoweidlem11  40228  stoweidlem26  40243  stoweidlem34  40251  stirlinglem5  40295  fourierdlem11  40335  fourierdlem12  40336  fourierdlem14  40338  fourierdlem15  40339  fourierdlem24  40348  fourierdlem25  40349  fourierdlem36  40360  fourierdlem37  40361  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem64  40387  fourierdlem69  40392  fourierdlem73  40396  fourierdlem79  40402  fourierdlem81  40404  fourierdlem92  40415  fourierdlem93  40416  fourierdlem111  40434  elaa2lem  40450  etransclem3  40454  etransclem7  40458  etransclem10  40461  etransclem24  40475  etransclem27  40478  etransclem35  40486  etransclem44  40495  etransclem46  40497  etransclem47  40498  etransclem48  40499  2ffzoeq  41338  iccpartigtl  41359  iccpartltu  41361  iccpartgt  41363  pfxnd  41395  pfxccatin12lem1  41423  0even  41931  2zrngamgm  41939  altgsumbcALT  42131  expnegico01  42308  dig0  42400  nn0sumshdiglem2  42416