MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0z Unicode version

Theorem 0z 10900
Description: Zero is an integer. (Contributed by NM, 12-Jan-2002.)
Assertion
Ref Expression
0z

Proof of Theorem 0z
StepHypRef Expression
1 0re 9617 . 2
2 eqid 2457 . . 3
323mix1i 1168 . 2
4 elz 10891 . 2
51, 3, 4mpbir2an 920 1
Colors of variables: wff setvar class
Syntax hints:  \/w3o 972  =wceq 1395  e.wcel 1818   cr 9512  0cc0 9513  -ucneg 9829   cn 10561   cz 10889
This theorem is referenced by:  0zd  10901  elnn0z  10902  nn0ssz  10910  znegcl  10924  zgt0ge1  10942  nn0lt10bOLD  10951  nnm1ge0  10956  gtndiv  10965  zeo  10973  nn0ind  10984  fnn0ind  10988  eluzadd  11138  eluzsub  11139  nn0uz  11144  1eluzge0  11153  2eluzge0OLD  11155  nn0infm  11192  eqreznegel  11196  fz10  11735  fz01en  11742  fzshftral  11795  fznn0  11799  fz0tp  11806  elfz0ubfz0  11807  1fv  11821  lbfzo0  11862  elfzonlteqm1  11891  fzo01  11897  fzo0to2pr  11899  fzo0to3tp  11900  flge0nn0  11954  btwnzge0  11961  zmodfz  12017  modid  12020  zmodid2  12024  ltweuz  12072  uzenom  12075  fzennn  12078  cardfz  12080  hashgf1o  12081  f13idfv  12106  seqfn  12119  seq1  12120  seqp1  12122  exp0  12170  bcnn  12390  bcm1k  12393  bcval5  12396  bcpasc  12399  hashgadd  12445  hashbc  12502  fz1isolem  12510  hashge2el2dif  12521  brfi1uzind  12532  lswccat0lsw  12608  eqs1  12621  s111  12623  swrdlend  12656  swrd0  12658  wrdeqswrdlsw  12674  swrds1  12676  repswswrd  12756  cshw0  12765  s2f1o  12864  f1oun2prg  12865  rexfiuz  13180  climz  13372  climaddc1  13457  climmulc2  13459  climsubc1  13460  climsubc2  13461  climlec2  13481  sumss  13546  binomlem  13641  binom  13642  bcxmas  13647  climcndslem1  13661  arisum2  13672  explecnv  13676  geomulcvg  13685  ef0lem  13814  efcvgfsum  13821  ege2le3  13825  eftlub  13844  efgt1p2  13849  efgt1p  13850  ruclem4  13967  ruclem6  13968  nthruc  13984  dvds0  13999  0dvds  14004  fsumdvds  14029  odd2np1lem  14045  divalglem6  14056  divalglem7  14057  divalglem8  14058  bitsfzo  14085  bitsmod  14086  0bits  14089  m1bits  14090  sadc0  14104  smup0  14129  gcd0val  14147  gcddvds  14153  gcd0id  14161  gcdid0  14162  gcdaddm  14167  gcdid  14169  bezoutlem1  14176  bezout  14180  dfphi2  14304  phiprmpw  14306  prmdiveq  14316  prmdivdiv  14317  pc0  14378  pcdvdstr  14399  pcfaclem  14417  prmreclem2  14435  prmreclem4  14437  zgz  14451  igz  14452  4sqlem19  14481  vdwap0  14494  ramz  14543  1259lem1  14613  1259lem4  14616  2503lem2  14620  4001lem1  14623  4001lem3  14625  gsumws1  16007  mulg0  16147  dfod2  16586  zaddablx  16876  0cyg  16895  srgbinomlem4  17194  srgbinom  17196  psrbaglefi  18023  psrbaglefiOLD  18024  ltbwe  18137  zring0  18498  zrng0  18505  zndvds0  18589  pmatcollpw3fi1lem1  19287  pmatcollpw3fi1  19289  iscmet3lem3  21729  vitalilem1  22017  iblcnlem1  22194  itgcnlem  22196  dvn0  22327  dvexp3  22379  plyco  22638  0dgr  22642  0dgrb  22643  coefv0  22645  coemulc  22652  vieta1lem2  22707  vieta1  22708  elqaalem1  22715  elqaalem3  22717  aareccl  22722  aannenlem1  22724  aannenlem2  22725  aalioulem1  22728  taylfval  22754  taylplem1  22758  taylplem2  22759  taylpfval  22760  dvtaylp  22765  dvradcnv  22816  pserulm  22817  pserdvlem2  22823  abelthlem6  22831  abelthlem9  22835  logf1o2  23031  advlogexp  23036  ang180lem3  23143  1cubr  23173  leibpi  23273  log2ublem3  23279  fsumharmonic  23341  wilthlem1  23342  muf  23414  0sgm  23418  1sgmprm  23474  ppiub  23479  bposlem1  23559  bposlem2  23560  lgslem2  23572  lgsfcl2  23577  lgsval2lem  23581  lgs0  23584  lgsdir2lem3  23600  lgsdirnn0  23614  lgsdinn0  23615  pntrlog2bndlem4  23765  padicabv  23815  ostth2lem2  23819  usgraexvlem  24395  usgraexmpldifpr  24400  usgraexmpl  24401  2trllemD  24559  2trllemG  24560  wlkntrllem2  24562  wlkntrl  24564  0pth  24572  0spth  24573  constr1trl  24590  constr2spthlem1  24596  usgrcyclnl1  24640  3v3e3cycl1  24644  constr3lem4  24647  constr3trllem3  24652  constr3trllem5  24654  wlkv0  24760  eupa0  24974  eupares  24975  gx0  25263  zaddsubgo  25356  zringnm  27940  zzsnmOLD  27942  qqh0  27965  qqhcn  27972  qqhucn  27973  eulerpartlemmf  28314  ballotlem2  28427  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemodife  28436  plymulx0  28504  signstf0  28525  signsvf0  28537  subfacval2  28631  cvmliftlem4  28733  cvmliftlem5  28734  relexp0  29052  fz0n  29110  4bc2eq6  29112  risefall0lem  29148  binomfallfac  29163  bpoly1  29813  bpolydiflem  29816  bpoly2  29819  bpoly3  29820  bpoly4  29821  sdclem1  30236  heibor1lem  30305  heiborlem4  30310  mzpnegmpt  30676  diophrw  30692  vdioph  30713  diophren  30747  irrapxlem1  30758  rmxy0  30859  monotoddzzfi  30878  zindbi  30882  rmyeq0  30891  jm2.18  30930  jm2.15nn0  30945  jm2.16nn0  30946  mpaaeu  31099  lcm0val  31200  dvdslcm  31204  lcmeq0  31206  lcmgcd  31213  lcmdvds  31214  nzss  31222  hashnzfz2  31226  dvradcnv2  31252  binomcxplemnn0  31254  binomcxplemrat  31255  binomcxplemnotnn0  31261  halffl  31493  fz1ssfz0  31510  dvnmul  31740  stoweidlem11  31793  stoweidlem17  31799  stoweidlem26  31808  stoweidlem34  31816  stirlinglem7  31862  fourierdlem20  31909  etransclem25  32042  etransclem26  32043  etransclem37  32054  2ffzoeq  32341  1odd  32499  0even  32737  2zrngamgm  32745  altgsumbcALT  32942  aacllem  33216  bj-flbi3  34608
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-i2m1 9581  ax-1ne0 9582  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299  df-neg 9831  df-z 10890
  Copyright terms: Public domain W3C validator