Theorem 0z 9468

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 8157	. 2 |- 0 e. RR
2		eqid 2229	. . 3 |- 0 = 0
3	2	3mix1i 1193	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9459	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 948	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 1001   = wceq 1395   e. wcel 2200   RRcr 8009   0cc0 8010   -ucneg 8329   NNcn 9121   ZZcz 9457

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8104  ax-addrcl 8107  ax-rnegex 8119

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010  df-neg 8331  df-z 9458

This theorem is referenced by:  0zd  9469  nn0ssz  9475  znegcl  9488  nnnle0  9506  zgt0ge1  9516  nn0n0n1ge2b  9537  nn0lt10b  9538  nnm1ge0  9544  gtndiv  9553  msqznn  9558  zeo  9563  nn0ind  9572  fnn0ind  9574  nn0uz  9769  1eluzge0  9781  elnn0dc  9818  eqreznegel  9821  qreccl  9849  qdivcl  9850  irrmul  9854  irrmulap  9855  fz10  10254  fz01en  10261  fzpreddisj  10279  fzshftral  10316  fznn0  10321  fz1ssfz0  10325  fz0sn  10329  fz0tp  10330  fz0to3un2pr  10331  fz0to4untppr  10332  elfz0ubfz0  10333  1fv  10347  fzo0n  10376  lbfzo0  10393  elfzonlteqm1  10428  fzo01  10434  fzo0to2pr  10436  fzo0to3tp  10437  flqge0nn0  10525  divfl0  10528  btwnzge0  10532  modqmulnn  10576  zmodfz  10580  modqid  10583  zmodid2  10586  q0mod  10589  modqmuladdnn0  10602  frecfzennn  10660  xnn0nnen  10671  qexpclz  10794  qsqeqor  10884  facdiv  10972  bcval  10983  bcnn  10991  bcm1k  10994  bcval5  10997  bcpasc  11000  4bc2eq6  11008  hashinfom  11012  iswrd  11086  iswrdiz  11091  wrdexg  11095  wrdfin  11103  wrdnval  11115  wrdred1hash  11128  lsw0  11132  ccatsymb  11150  ccatalpha  11161  s111  11179  ccat1st1st  11187  fzowrddc  11194  swrdlen  11199  swrdnd  11206  swrdwrdsymbg  11211  swrds1  11215  pfxval  11221  pfx00g  11222  pfx0g  11223  fnpfx  11224  pfxlen  11232  swrdccatin1  11272  swrdccat  11282  swrdccat3blem  11286  rexfiuz  11515  qabsor  11601  nn0abscl  11611  nnabscl  11626  climz  11818  climaddc1  11855  climmulc2  11857  climsubc1  11858  climsubc2  11859  climlec2  11867  binomlem  12009  binom  12010  bcxmas  12015  arisum2  12025  explecnv  12031  ef0lem  12186  dvdsval2  12316  dvdsdc  12324  moddvds  12325  dvds0  12332  0dvds  12337  zdvdsdc  12338  dvdscmulr  12346  dvdsmulcr  12347  fsumdvds  12368  dvdslelemd  12369  dvdsabseq  12373  divconjdvds  12375  alzdvds  12380  fzo0dvdseq  12383  odd2np1lem  12398  bitsfzo  12481  bitsmod  12482  0bits  12485  m1bits  12486  bitsinv1lem  12487  bitsinv1  12488  gcdmndc  12491  gcdsupex  12493  gcdsupcl  12494  gcd0val  12496  gcddvds  12499  gcd0id  12515  gcdid0  12516  gcdid  12522  bezoutlema  12535  bezoutlemb  12536  bezoutlembi  12541  dfgcd3  12546  dfgcd2  12550  gcdmultiplez  12557  dvdssq  12567  algcvgblem  12586  lcmmndc  12599  lcm0val  12602  dvdslcm  12606  lcmeq0  12608  lcmgcd  12615  lcmdvds  12616  lcmid  12617  3lcm2e6woprm  12623  6lcm4e12  12624  cncongr2  12641  sqrt2irrap  12717  dfphi2  12757  phiprmpw  12759  crth  12761  phimullem  12762  eulerthlemfi  12765  hashgcdeq  12777  phisum  12778  pceu  12833  pcdiv  12840  pc0  12842  pcqdiv  12845  pcexp  12847  pcxnn0cl  12848  pcxcl  12849  pcxqcl  12850  pcdvdstr  12865  dvdsprmpweqnn  12874  pcaddlem  12877  pcadd  12878  pcfaclem  12887  qexpz  12890  zgz  12911  igz  12912  4sqlem19  12947  ennnfonelemjn  12988  ennnfonelem1  12993  mulg0  13677  subgmulg  13740  zring0  14579  zndvds0  14629  znf1o  14630  znfi  14634  znhash  14635  psr1clfi  14667  plycolemc  15447  rpcxp0  15587  0sgm  15674  1sgmprm  15683  lgslem2  15695  lgsfcl2  15700  lgs0  15707  lgsneg  15718  lgsdilem  15721  lgsdir2lem3  15724  lgsdir  15729  lgsdilem2  15730  lgsdi  15731  lgsne0  15732  lgsprme0  15736  lgsdirnn0  15741  lgsdinn0  15742  wlkv0  16110  wlklenvclwlk  16114  upgr2wlkdc  16116  clwwlkccatlem  16137  apdifflemr  16475  apdiff  16476  iswomni0  16479  nconstwlpolem  16493