Theorem 0z 9383

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 8072	. 2 |- 0 e. RR
2		eqid 2205	. . 3 |- 0 = 0
3	2	3mix1i 1172	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9374	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 945	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 980   = wceq 1373   e. wcel 2176   RRcr 7924   0cc0 7925   -ucneg 8244   NNcn 9036   ZZcz 9372

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-1re 8019  ax-addrcl 8022  ax-rnegex 8034

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-rab 2493  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-iota 5232  df-fv 5279  df-ov 5947  df-neg 8246  df-z 9373

This theorem is referenced by:  0zd  9384  nn0ssz  9390  znegcl  9403  nnnle0  9421  zgt0ge1  9431  nn0n0n1ge2b  9452  nn0lt10b  9453  nnm1ge0  9459  gtndiv  9468  msqznn  9473  zeo  9478  nn0ind  9487  fnn0ind  9489  nn0uz  9683  1eluzge0  9695  elnn0dc  9732  eqreznegel  9735  qreccl  9763  qdivcl  9764  irrmul  9768  irrmulap  9769  fz10  10168  fz01en  10175  fzpreddisj  10193  fzshftral  10230  fznn0  10235  fz1ssfz0  10239  fz0sn  10243  fz0tp  10244  fz0to3un2pr  10245  fz0to4untppr  10246  elfz0ubfz0  10247  1fv  10261  fzo0n  10290  lbfzo0  10305  elfzonlteqm1  10339  fzo01  10345  fzo0to2pr  10347  fzo0to3tp  10348  flqge0nn0  10436  divfl0  10439  btwnzge0  10443  modqmulnn  10487  zmodfz  10491  modqid  10494  zmodid2  10497  q0mod  10500  modqmuladdnn0  10513  frecfzennn  10571  xnn0nnen  10582  qexpclz  10705  qsqeqor  10795  facdiv  10883  bcval  10894  bcnn  10902  bcm1k  10905  bcval5  10908  bcpasc  10911  4bc2eq6  10919  hashinfom  10923  iswrd  10996  iswrdiz  11001  wrdexg  11005  wrdfin  11013  wrdnval  11024  wrdred1hash  11037  lsw0  11041  ccatsymb  11058  s111  11085  ccat1st1st  11093  fzowrddc  11100  swrdlen  11105  swrdnd  11112  swrdwrdsymbg  11117  swrds1  11121  rexfiuz  11300  qabsor  11386  nn0abscl  11396  nnabscl  11411  climz  11603  climaddc1  11640  climmulc2  11642  climsubc1  11643  climsubc2  11644  climlec2  11652  binomlem  11794  binom  11795  bcxmas  11800  arisum2  11810  explecnv  11816  ef0lem  11971  dvdsval2  12101  dvdsdc  12109  moddvds  12110  dvds0  12117  0dvds  12122  zdvdsdc  12123  dvdscmulr  12131  dvdsmulcr  12132  fsumdvds  12153  dvdslelemd  12154  dvdsabseq  12158  divconjdvds  12160  alzdvds  12165  fzo0dvdseq  12168  odd2np1lem  12183  bitsfzo  12266  bitsmod  12267  0bits  12270  m1bits  12271  bitsinv1lem  12272  bitsinv1  12273  gcdmndc  12276  gcdsupex  12278  gcdsupcl  12279  gcd0val  12281  gcddvds  12284  gcd0id  12300  gcdid0  12301  gcdid  12307  bezoutlema  12320  bezoutlemb  12321  bezoutlembi  12326  dfgcd3  12331  dfgcd2  12335  gcdmultiplez  12342  dvdssq  12352  algcvgblem  12371  lcmmndc  12384  lcm0val  12387  dvdslcm  12391  lcmeq0  12393  lcmgcd  12400  lcmdvds  12401  lcmid  12402  3lcm2e6woprm  12408  6lcm4e12  12409  cncongr2  12426  sqrt2irrap  12502  dfphi2  12542  phiprmpw  12544  crth  12546  phimullem  12547  eulerthlemfi  12550  hashgcdeq  12562  phisum  12563  pceu  12618  pcdiv  12625  pc0  12627  pcqdiv  12630  pcexp  12632  pcxnn0cl  12633  pcxcl  12634  pcxqcl  12635  pcdvdstr  12650  dvdsprmpweqnn  12659  pcaddlem  12662  pcadd  12663  pcfaclem  12672  qexpz  12675  zgz  12696  igz  12697  4sqlem19  12732  ennnfonelemjn  12773  ennnfonelem1  12778  mulg0  13461  subgmulg  13524  zring0  14362  zndvds0  14412  znf1o  14413  znfi  14417  znhash  14418  psr1clfi  14450  plycolemc  15230  rpcxp0  15370  0sgm  15457  1sgmprm  15466  lgslem2  15478  lgsfcl2  15483  lgs0  15490  lgsneg  15501  lgsdilem  15504  lgsdir2lem3  15507  lgsdir  15512  lgsdilem2  15513  lgsdi  15514  lgsne0  15515  lgsprme0  15519  lgsdirnn0  15524  lgsdinn0  15525  apdifflemr  15986  apdiff  15987  iswomni0  15990  nconstwlpolem  16004