Theorem 0z 9490

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 8179	. 2 |- 0 e. RR
2		eqid 2231	. . 3 |- 0 = 0
3	2	3mix1i 1195	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9481	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 950	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 1003   = wceq 1397   e. wcel 2202   RRcr 8031   0cc0 8032   -ucneg 8351   NNcn 9143   ZZcz 9479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1re 8126  ax-addrcl 8129  ax-rnegex 8141

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021  df-neg 8353  df-z 9480

This theorem is referenced by:  0zd  9491  nn0ssz  9497  znegcl  9510  nnnle0  9528  zgt0ge1  9538  nn0n0n1ge2b  9559  nn0lt10b  9560  nnm1ge0  9566  gtndiv  9575  msqznn  9580  zeo  9585  nn0ind  9594  fnn0ind  9596  nn0uz  9791  1eluzge0  9808  elnn0dc  9845  eqreznegel  9848  qreccl  9876  qdivcl  9877  irrmul  9881  irrmulap  9882  fz10  10281  fz01en  10288  fzpreddisj  10306  fzshftral  10343  fznn0  10348  fz1ssfz0  10352  fz0sn  10356  fz0tp  10357  fz0to3un2pr  10358  fz0to4untppr  10359  elfz0ubfz0  10360  1fv  10374  fzo0n  10403  lbfzo0  10420  elfzonlteqm1  10456  fzo01  10462  fzo0to2pr  10464  fzo0to3tp  10465  flqge0nn0  10554  divfl0  10557  btwnzge0  10561  modqmulnn  10605  zmodfz  10609  modqid  10612  zmodid2  10615  q0mod  10618  modqmuladdnn0  10631  frecfzennn  10689  xnn0nnen  10700  qexpclz  10823  qsqeqor  10913  facdiv  11001  bcval  11012  bcnn  11020  bcm1k  11023  bcval5  11026  bcpasc  11029  4bc2eq6  11037  hashinfom  11041  iswrd  11119  iswrdiz  11124  wrdexg  11128  wrdfin  11136  wrdnval  11148  wrdred1hash  11161  lsw0  11165  ccatsymb  11183  ccatalpha  11194  s111  11212  ccat1st1st  11222  fzowrddc  11232  swrdlen  11237  swrdnd  11244  swrdwrdsymbg  11249  swrds1  11253  pfxval  11259  pfx00g  11260  pfx0g  11261  fnpfx  11262  pfxlen  11270  swrdccatin1  11310  swrdccat  11320  swrdccat3blem  11324  rexfiuz  11554  qabsor  11640  nn0abscl  11650  nnabscl  11665  climz  11857  climaddc1  11894  climmulc2  11896  climsubc1  11897  climsubc2  11898  climlec2  11906  binomlem  12049  binom  12050  bcxmas  12055  arisum2  12065  explecnv  12071  ef0lem  12226  dvdsval2  12356  dvdsdc  12364  moddvds  12365  dvds0  12372  0dvds  12377  zdvdsdc  12378  dvdscmulr  12386  dvdsmulcr  12387  fsumdvds  12408  dvdslelemd  12409  dvdsabseq  12413  divconjdvds  12415  alzdvds  12420  fzo0dvdseq  12423  odd2np1lem  12438  bitsfzo  12521  bitsmod  12522  0bits  12525  m1bits  12526  bitsinv1lem  12527  bitsinv1  12528  gcdmndc  12531  gcdsupex  12533  gcdsupcl  12534  gcd0val  12536  gcddvds  12539  gcd0id  12555  gcdid0  12556  gcdid  12562  bezoutlema  12575  bezoutlemb  12576  bezoutlembi  12581  dfgcd3  12586  dfgcd2  12590  gcdmultiplez  12597  dvdssq  12607  algcvgblem  12626  lcmmndc  12639  lcm0val  12642  dvdslcm  12646  lcmeq0  12648  lcmgcd  12655  lcmdvds  12656  lcmid  12657  3lcm2e6woprm  12663  6lcm4e12  12664  cncongr2  12681  sqrt2irrap  12757  dfphi2  12797  phiprmpw  12799  crth  12801  phimullem  12802  eulerthlemfi  12805  hashgcdeq  12817  phisum  12818  pceu  12873  pcdiv  12880  pc0  12882  pcqdiv  12885  pcexp  12887  pcxnn0cl  12888  pcxcl  12889  pcxqcl  12890  pcdvdstr  12905  dvdsprmpweqnn  12914  pcaddlem  12917  pcadd  12918  pcfaclem  12927  qexpz  12930  zgz  12951  igz  12952  4sqlem19  12987  ennnfonelemjn  13028  ennnfonelem1  13033  mulg0  13717  subgmulg  13780  zring0  14620  zndvds0  14670  znf1o  14671  znfi  14675  znhash  14676  psr1clfi  14708  plycolemc  15488  rpcxp0  15628  0sgm  15715  1sgmprm  15724  lgslem2  15736  lgsfcl2  15741  lgs0  15748  lgsneg  15759  lgsdilem  15762  lgsdir2lem3  15765  lgsdir  15770  lgsdilem2  15771  lgsdi  15772  lgsne0  15773  lgsprme0  15777  lgsdirnn0  15782  lgsdinn0  15783  usgrexmpldifpr  16106  vdegp1bid  16172  wlkv0  16226  wlklenvclwlk  16230  upgr2wlkdc  16234  clwwlkccatlem  16257  eupthfi  16308  trlsegvdeglem6  16322  apdifflemr  16677  apdiff  16678  qdiff  16679  iswomni0  16682  nconstwlpolem  16696