MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0zd Structured version   Visualization version   GIF version

Theorem 0zd 11636
Description: Zero is an integer, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
0zd (𝜑 → 0 ∈ ℤ)

Proof of Theorem 0zd
StepHypRef Expression
1 0z 11635 . 2 0 ∈ ℤ
21a1i 11 1 (𝜑 → 0 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2155  0cc0 10189  cz 11624
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-1cn 10247  ax-addrcl 10250  ax-rnegex 10260  ax-cnre 10262
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-iota 6031  df-fv 6076  df-ov 6845  df-neg 10523  df-z 11625
This theorem is referenced by:  fzctr  12659  fzosubel3  12737  bcval5  13309  snopiswrd  13495  wrdsymb0  13520  ccatsymb  13553  swrdspsleq  13651  pfxnd  13676  pfxccatin12lem1  13732  swrdccatin12lem2bOLD  13733  swrdccat  13743  swrdccatOLD  13744  repswswrd  13808  eqwrds3  13993  fzomaxdiflem  14369  fsumzcl  14753  isumnn0nn  14860  climcndslem1  14867  climcnds  14869  harmonic  14877  geolim  14887  geolim2  14888  geoisum  14894  geoisumr  14895  mertenslem1  14901  mertenslem2  14902  mertens  14903  risefacval2  15025  fallfacval2  15026  binomfallfaclem2  15055  bpolydiflem  15069  eff  15096  efcvg  15099  reefcl  15101  efcj  15106  eftlub  15123  effsumlt  15125  eflegeo  15135  eirrlem  15216  ruclem6  15248  dvdsmodexp  15275  dvdsmod  15337  pwp1fsum  15398  bitsinv1lem  15446  sadcf  15458  sadadd3  15466  smupf  15483  alginv  15571  algcvg  15572  algcvga  15575  algfx  15576  eucalgcvga  15582  eucalg  15583  lcmftp  15632  phiprmpw  15762  iserodd  15821  pcpre1  15828  qexpz  15886  prmreclem4  15904  vdwapun  15959  odf1  18245  srgbinomlem4  18810  evlslem1  19788  cpmadugsumlemF  20960  dvnff  23977  dgrcl  24280  dgrub  24281  dgrlb  24283  elqaalem2  24366  elqaalem3  24367  geolim3  24385  tayl0  24407  dvtaylp  24415  radcnvlem1  24458  radcnvlem3  24460  radcnv0  24461  radcnvlt2  24464  pserulm  24467  psercn2  24468  pserdvlem2  24473  pserdv2  24475  abelthlem4  24479  abelthlem5  24480  abelthlem6  24481  abelthlem7  24483  abelthlem8  24484  abelthlem9  24485  cosne0  24568  logtayl  24697  leibpi  24960  leibpisum  24961  log2cnv  24962  log2tlbnd  24963  basellem3  25100  dchrptlem2  25281  bcmono  25293  lgsne0  25351  crctcshwlkn0lem3  26996  archiabllem1b  30128  oddpwdc  30798  ballotlemfval0  30940  fsum2dsub  31068  breprexplemc  31093  breprexp  31094  circlemeth  31101  fwddifnp1  32648  knoppcnlem6  32859  knoppcnlem9  32862  knoppcn  32865  knoppndvlem2  32875  knoppndvlem4  32877  knoppf  32897  itg2addnclem2  33817  rmynn  38132  jm2.24nn  38135  jm2.17c  38138  jm2.24  38139  acongrep  38156  acongeq  38159  jm2.18  38164  jm2.23  38172  jm2.20nn  38173  jm2.27a  38181  jm2.27c  38183  rmydioph  38190  hashnzfz  39125  bccbc  39150  binomcxplemnn0  39154  binomcxplemrat  39155  binomcxplemnotnn0  39161  mccllem  40399  expfac  40459  0cnv  40544  lmbr3v  40547  sinaover2ne0  40649  dvnmul  40728  dvnprodlem1  40731  dvnprodlem2  40732  stoweidlem11  40797  stoweidlem26  40812  stoweidlem34  40820  stirlinglem5  40864  fourierdlem11  40904  fourierdlem12  40905  fourierdlem14  40907  fourierdlem15  40908  fourierdlem24  40917  fourierdlem25  40918  fourierdlem36  40929  fourierdlem37  40930  fourierdlem41  40934  fourierdlem48  40940  fourierdlem49  40941  fourierdlem50  40942  fourierdlem64  40956  fourierdlem69  40961  fourierdlem73  40965  fourierdlem79  40971  fourierdlem81  40973  fourierdlem92  40984  fourierdlem93  40985  fourierdlem111  41003  elaa2lem  41019  etransclem3  41023  etransclem7  41027  etransclem10  41030  etransclem24  41044  etransclem27  41047  etransclem35  41055  etransclem44  41064  etransclem46  41066  etransclem47  41067  etransclem48  41068  2ffzoeq  42004  iccpartigtl  42025  iccpartltu  42027  iccpartgt  42029  0even  42532  2zrngamgm  42540  altgsumbcALT  42732  expnegico01  42909  dig0  43001  nn0sumshdiglem2  43017
  Copyright terms: Public domain W3C validator