Theorem 0z 11388

Description: Zero is an integer. (Contributed by NM, 12-Jan-2002.)

Assertion

Ref	Expression
0z	|- 0 e. ZZ

Proof of Theorem 0z

Step	Hyp	Ref	Expression
1		0re 10040	. 2 |- 0 e. RR
2		eqid 2622	. . 3 |- 0 = 0
3	2	3mix1i 1233	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 11379	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 955	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 1036   = wceq 1483   e. wcel 1990   RRcr 9935   0cc0 9936   -ucneg 10267   NNcn 11020   ZZcz 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:  0zd  11389  elnn0z  11390  nn0ssz  11398  znegcl  11412  zgt0ge1  11431  nnm1ge0  11445  gtndiv  11454  zeo  11463  nn0ind  11472  fnn0ind  11476  eluzadd  11716  eluzsub  11717  nn0uz  11722  1eluzge0  11732  nn0inf  11770  eqreznegel  11774  fz10  12362  fz01en  12369  fzshftral  12428  fznn0  12432  fz0sn  12439  fz0tp  12440  fz0to3un2pr  12441  fz0to4untppr  12442  elfz0ubfz0  12443  fz0sn0fz1  12456  1fv  12458  fzo0n  12490  lbfzo0  12507  elfzonlteqm1  12543  fzo01  12550  fzo0to2pr  12553  fzo0to3tp  12554  ico01fl0  12620  flge0nn0  12621  divfl0  12625  btwnzge0  12629  zmodfz  12692  modid  12695  zmodid2  12698  modmuladdnn0  12714  ltweuz  12760  uzenom  12763  fzennn  12767  cardfz  12769  hashgf1o  12770  f13idfv  12800  seqfn  12813  seq1  12814  seqp1  12816  exp0  12864  bcnn  13099  bcm1k  13102  bcval5  13105  bcpasc  13108  4bc2eq6  13116  hashgadd  13166  hashbc  13237  fz1isolem  13245  hashge2el2dif  13262  fi1uzind  13279  fi1uzindOLD  13285  s111  13395  swrdnd  13432  swrds1  13451  repswswrd  13531  cshw0  13540  s2f1o  13661  f1oun2prg  13662  rexfiuz  14087  climz  14280  climaddc1  14365  climmulc2  14367  climsubc1  14368  climsubc2  14369  climlec2  14389  sumss  14455  binomlem  14561  binom  14562  bcxmas  14567  climcndslem1  14581  arisum2  14593  explecnv  14597  geomulcvg  14607  risefall0lem  14757  binomfallfac  14772  bpoly1  14782  bpolydiflem  14785  bpoly2  14788  bpoly3  14789  bpoly4  14790  ef0lem  14809  efcvgfsum  14816  ege2le3  14820  eftlub  14839  efgt1p2  14844  efgt1p  14845  ruclem4  14963  ruclem6  14964  nthruc  14981  dvds0  14997  0dvds  15002  fsumdvds  15030  odd2np1lem  15064  divalglem6  15121  divalglem7  15122  divalglem8  15123  bitsfzo  15157  bitsmod  15158  0bits  15161  m1bits  15162  sadc0  15176  smup0  15201  gcd0val  15219  gcddvds  15225  gcd0id  15240  gcdid0  15241  gcdaddm  15246  gcdid  15248  bezoutlem1  15256  bezout  15260  dfgcd2  15263  lcm0val  15307  dvdslcm  15311  lcmeq0  15313  lcmgcd  15320  lcmdvds  15321  lcmftp  15349  lcmfunsnlem2  15353  dfphi2  15479  phiprmpw  15481  prmdiveq  15491  prmdivdiv  15492  pc0  15559  pcdvdstr  15580  dvdsprmpweqnn  15589  pcfaclem  15602  prmreclem2  15621  prmreclem4  15623  zgz  15637  igz  15638  4sqlem19  15667  vdwap0  15680  ramz  15729  1259lem1  15838  1259lem4  15841  2503lem2  15845  4001lem1  15848  4001lem3  15850  gsumws1  17376  mulg0  17546  dfod2  17981  zaddablx  18275  0cyg  18294  srgbinomlem4  18543  srgbinom  18545  ltbwe  19472  zring0  19828  zndvds0  19899  pmatcollpw3fi1lem1  20591  pmatcollpw3fi1  20593  iscmet3lem3  23088  vitalilem1  23376  vitalilem1OLD  23377  iblcnlem1  23554  itgcnlem  23556  dvn0  23687  dvexp3  23741  plyco  23997  0dgr  24001  0dgrb  24002  coefv0  24004  coemulc  24011  vieta1lem2  24066  vieta1  24067  elqaalem1  24074  elqaalem3  24076  aareccl  24081  aannenlem1  24083  aannenlem2  24084  aalioulem1  24087  taylfval  24113  taylplem1  24117  taylplem2  24118  taylpfval  24119  dvtaylp  24124  dvradcnv  24175  pserulm  24176  pserdvlem2  24182  abelthlem6  24190  abelthlem9  24194  logf1o2  24396  advlogexp  24401  ang180lem3  24541  1cubr  24569  leibpi  24669  fsumharmonic  24738  wilthlem1  24794  muf  24866  0sgm  24870  1sgmprm  24924  ppiub  24929  bposlem1  25009  bposlem2  25010  lgslem2  25023  lgsfcl2  25028  lgsval2lem  25032  lgs0  25035  lgsdir2lem3  25052  lgsdirnn0  25069  lgsdinn0  25070  pntrlog2bndlem4  25269  padicabv  25319  ostth2lem2  25323  usgrexmpldifpr  26150  usgrexmplef  26151  wlkv0  26547  spthispth  26622  uhgrwkspthlem2  26650  pthdlem2  26664  0ewlk  26975  0wlkons1  26982  0pth  26986  0pthon  26988  wlk2v2elem2  27016  ntrl2v2e  27018  0dp2dp  29617  zringnm  30004  qqh0  30028  qqhcn  30035  qqhucn  30036  rrh0  30059  eulerpartlemmf  30437  ballotlem2  30550  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemodife  30559  plymulx0  30624  signstf0  30645  signsvf0  30657  hgt750lemd  30726  hgt750lem  30729  subfacval2  31169  cvmliftlem4  31270  cvmliftlem5  31271  fz0n  31616  bcneg1  31622  bccolsum  31625  fwddifn0  32271  fwddifnp1  32272  knoppcnlem8  32490  knoppcnlem11  32493  poimirlem24  33433  poimirlem27  33436  poimirlem28  33437  sdclem1  33539  heibor1lem  33608  heiborlem4  33613  mzpnegmpt  37307  diophrw  37322  vdioph  37343  diophren  37377  irrapxlem1  37386  rmxy0  37488  monotoddzzfi  37507  zindbi  37511  rmyeq0  37520  jm2.18  37555  jm2.15nn0  37570  jm2.16nn0  37571  mpaaeu  37720  nzss  38516  hashnzfz2  38520  dvradcnv2  38546  binomcxplemnn0  38548  binomcxplemrat  38549  binomcxplemnotnn0  38555  halffl  39510  fz1ssfz0  39524  lmbr3v  39977  dvnmul  40158  stoweidlem11  40228  stoweidlem17  40234  stoweidlem26  40243  stoweidlem34  40251  stirlinglem7  40297  fourierdlem20  40344  etransclem25  40476  etransclem26  40477  etransclem37  40488  smfmullem4  41001  2ffzoeq  41338  fmtnorec2  41455  0evenALTV  41599  0noddALTV  41600  1odd  41811  0even  41931  2zrngamgm  41939  altgsumbcALT  42131  blen1  42378  blen1b  42382  0dig1  42403  0dig2pr01  42404  nn0sumshdiglem1  42415  aacllem  42547