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

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

Proof of Theorem 0z
StepHypRef Expression
1 0re 9642 . 2  |-  0  e.  RR
2 eqid 2429 . . 3  |-  0  =  0
323mix1i 1177 . 2  |-  ( 0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN )
4 elz 10939 . 2  |-  ( 0  e.  ZZ  <->  ( 0  e.  RR  /\  (
0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN ) ) )
51, 3, 4mpbir2an 928 1  |-  0  e.  ZZ
Colors of variables: wff setvar class
Syntax hints:    \/ w3o 981    = wceq 1437    e. wcel 1870   RRcr 9537   0cc0 9538   -ucneg 9860   NNcn 10609   ZZcz 10937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-i2m1 9606  ax-1ne0 9607  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308  df-neg 9862  df-z 10938
This theorem is referenced by:  0zd  10949  elnn0z  10950  nn0ssz  10958  znegcl  10972  zgt0ge1  10990  nn0lt10bOLD  10999  nnm1ge0  11004  gtndiv  11013  zeo  11021  nn0ind  11030  fnn0ind  11034  eluzadd  11187  eluzsub  11188  nn0uz  11193  1eluzge0  11202  2eluzge0OLD  11204  nn0inf  11241  nn0infmOLD  11243  eqreznegel  11249  fz10  11818  fz01en  11825  fzshftral  11880  fznn0  11884  fz0tp  11891  elfz0ubfz0  11892  1fv  11906  fzo0n  11938  lbfzo0  11953  elfzonlteqm1  11986  fzo01  11992  fzo0to2pr  11995  fzo0to3tp  11996  ico01fl0  12050  flge0nn0  12051  btwnzge0  12058  zmodfz  12115  modid  12118  zmodid2  12122  ltweuz  12172  uzenom  12175  fzennn  12178  cardfz  12180  hashgf1o  12181  f13idfv  12209  seqfn  12222  seq1  12223  seqp1  12225  exp0  12273  bcnn  12494  bcm1k  12497  bcval5  12500  bcpasc  12503  4bc2eq6  12511  hashgadd  12553  hashbc  12611  fz1isolem  12619  hashge2el2dif  12630  brfi1uzind  12641  s111  12737  swrdnd  12773  swrds1  12792  repswswrd  12872  cshw0  12881  s2f1o  12980  f1oun2prg  12981  rexfiuz  13389  climz  13591  climaddc1  13676  climmulc2  13678  climsubc1  13679  climsubc2  13680  climlec2  13700  sumss  13768  binomlem  13865  binom  13866  bcxmas  13871  climcndslem1  13885  arisum2  13897  explecnv  13901  geomulcvg  13910  risefall0lem  14057  binomfallfac  14072  bpoly1  14082  bpolydiflem  14085  bpoly2  14088  bpoly3  14089  bpoly4  14090  ef0lem  14111  efcvgfsum  14118  ege2le3  14122  eftlub  14141  efgt1p2  14146  efgt1p  14147  ruclem4  14264  ruclem6  14265  nthruc  14281  dvds0  14296  0dvds  14301  fsumdvds  14326  odd2np1lem  14342  divalglem6  14354  divalglem7  14355  divalglem8  14356  bitsfzo  14383  bitsmod  14384  0bits  14387  m1bits  14388  sadc0  14402  smup0  14427  gcd0val  14445  gcddvds  14451  gcd0id  14461  gcdid0  14462  gcdaddm  14467  gcdid  14469  bezoutlem1  14477  bezout  14481  lcm0val  14529  dvdslcm  14534  lcmeq0  14536  lcmgcd  14543  lcmdvds  14544  lcmftp  14580  lcmfunsnlem2  14584  dfphi2  14691  phiprmpw  14693  prmdiveq  14703  prmdivdiv  14704  pc0  14767  pcdvdstr  14788  pcfaclem  14806  prmreclem2  14824  prmreclem4  14826  zgz  14840  igz  14841  4sqlem19  14876  vdwap0  14889  ramz  14946  1259lem1  15065  1259lem4  15068  2503lem2  15072  4001lem1  15075  4001lem3  15077  gsumws1  16574  mulg0  16714  dfod2  17153  zaddablx  17443  0cyg  17462  srgbinomlem4  17711  srgbinom  17713  psrbaglefi  18531  ltbwe  18631  zring0  18983  zndvds0  19052  pmatcollpw3fi1lem1  19741  pmatcollpw3fi1  19743  iscmet3lem3  22153  vitalilem1  22443  iblcnlem1  22622  itgcnlem  22624  dvn0  22755  dvexp3  22807  plyco  23063  0dgr  23067  0dgrb  23068  coefv0  23070  coemulc  23077  vieta1lem2  23132  vieta1  23133  elqaalem1  23140  elqaalem3  23142  aareccl  23147  aannenlem1  23149  aannenlem2  23150  aalioulem1  23153  taylfval  23179  taylplem1  23183  taylplem2  23184  taylpfval  23185  dvtaylp  23190  dvradcnv  23241  pserulm  23242  pserdvlem2  23248  abelthlem6  23256  abelthlem9  23260  logf1o2  23460  advlogexp  23465  ang180lem3  23605  1cubr  23633  leibpi  23733  log2ublem3  23739  fsumharmonic  23802  wilthlem1  23858  muf  23930  0sgm  23934  1sgmprm  23990  ppiub  23995  bposlem1  24075  bposlem2  24076  lgslem2  24088  lgsfcl2  24093  lgsval2lem  24097  lgs0  24100  lgsdir2lem3  24116  lgsdirnn0  24130  lgsdinn0  24131  pntrlog2bndlem4  24281  padicabv  24331  ostth2lem2  24335  usgraexvlem  24968  usgraexmpldifpr  24973  usgraexmpl  24974  2trllemD  25132  2trllemG  25133  wlkntrllem2  25135  wlkntrl  25137  0pth  25145  0spth  25146  constr1trl  25163  constr2spthlem1  25169  usgrcyclnl1  25213  3v3e3cycl1  25217  constr3lem4  25220  constr3trllem3  25225  constr3trllem5  25227  wlkv0  25333  eupa0  25547  eupares  25548  gx0  25834  zaddsubgo  25927  zringnm  28603  qqh0  28627  qqhcn  28634  qqhucn  28635  rrh0  28658  eulerpartlemmf  29034  ballotlem2  29147  ballotlemfc0  29151  ballotlemfcc  29152  ballotlemodife  29156  plymulx0  29224  signstf0  29245  signsvf0  29257  subfacval2  29698  cvmliftlem4  29799  cvmliftlem5  29800  fz0n  30151  bcneg1  30159  bccolsum  30162  fwddifn0  30716  fwddifnp1  30717  poimirlem24  31668  poimirlem27  31671  poimirlem28  31672  sdclem1  31776  heibor1lem  31845  heiborlem4  31850  mzpnegmpt  35295  diophrw  35310  vdioph  35331  diophren  35365  irrapxlem1  35376  rmxy0  35477  monotoddzzfi  35496  zindbi  35500  rmyeq0  35509  jm2.18  35549  jm2.15nn0  35564  jm2.16nn0  35565  mpaaeu  35715  nzss  36303  hashnzfz2  36307  dvradcnv2  36333  binomcxplemnn0  36335  binomcxplemrat  36336  binomcxplemnotnn0  36342  halffl  37122  fz1ssfz0  37137  dvnmul  37387  stoweidlem11  37440  stoweidlem17  37446  stoweidlem26  37455  stoweidlem34  37464  stirlinglem7  37511  fourierdlem20  37558  etransclem25  37691  etransclem26  37692  etransclem37  37703  0evenALTV  38207  0noddALTV  38208  2ffzoeq  38413  1odd  38569  0even  38689  2zrngamgm  38697  altgsumbcALT  38894  blen1  39156  blen1b  39160  0dig1  39181  0dig2pr01  39182  nn0sumshdiglem1  39193  aacllem  39301
  Copyright terms: Public domain W3C validator