Theorem 0z 9264

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 7957	. 2 |- 0 e. RR
2		eqid 2177	. . 3 |- 0 = 0
3	2	3mix1i 1169	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9255	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 942	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 977   = wceq 1353   e. wcel 2148   RRcr 7810   0cc0 7811   -ucneg 8129   NNcn 8919   ZZcz 9253

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1re 7905  ax-addrcl 7908  ax-rnegex 7920

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225  df-ov 5878  df-neg 8131  df-z 9254

This theorem is referenced by:  0zd  9265  nn0ssz  9271  znegcl  9284  zgt0ge1  9311  nn0n0n1ge2b  9332  nn0lt10b  9333  nnm1ge0  9339  gtndiv  9348  msqznn  9353  zeo  9358  nn0ind  9367  fnn0ind  9369  nn0uz  9562  1eluzge0  9574  elnn0dc  9611  eqreznegel  9614  qreccl  9642  qdivcl  9643  irrmul  9647  fz10  10046  fz01en  10053  fzpreddisj  10071  fzshftral  10108  fznn0  10113  fz1ssfz0  10117  fz0sn  10121  fz0tp  10122  fz0to3un2pr  10123  fz0to4untppr  10124  elfz0ubfz0  10125  1fv  10139  lbfzo0  10181  elfzonlteqm1  10210  fzo01  10216  fzo0to2pr  10218  fzo0to3tp  10219  flqge0nn0  10293  divfl0  10296  btwnzge0  10300  modqmulnn  10342  zmodfz  10346  modqid  10349  zmodid2  10352  q0mod  10355  modqmuladdnn0  10368  frecfzennn  10426  qexpclz  10541  qsqeqor  10631  facdiv  10718  bcval  10729  bcnn  10737  bcm1k  10740  bcval5  10743  bcpasc  10746  4bc2eq6  10754  hashinfom  10758  rexfiuz  10998  qabsor  11084  nn0abscl  11094  nnabscl  11109  climz  11300  climaddc1  11337  climmulc2  11339  climsubc1  11340  climsubc2  11341  climlec2  11349  binomlem  11491  binom  11492  bcxmas  11497  arisum2  11507  explecnv  11513  ef0lem  11668  dvdsval2  11797  dvdsdc  11805  moddvds  11806  dvds0  11813  0dvds  11818  zdvdsdc  11819  dvdscmulr  11827  dvdsmulcr  11828  dvdslelemd  11849  dvdsabseq  11853  divconjdvds  11855  alzdvds  11860  fzo0dvdseq  11863  odd2np1lem  11877  gcdmndc  11945  gcdsupex  11958  gcdsupcl  11959  gcd0val  11961  gcddvds  11964  gcd0id  11980  gcdid0  11981  gcdid  11987  bezoutlema  12000  bezoutlemb  12001  bezoutlembi  12006  dfgcd3  12011  dfgcd2  12015  gcdmultiplez  12022  dvdssq  12032  algcvgblem  12049  lcmmndc  12062  lcm0val  12065  dvdslcm  12069  lcmeq0  12071  lcmgcd  12078  lcmdvds  12079  lcmid  12080  3lcm2e6woprm  12086  6lcm4e12  12087  cncongr2  12104  sqrt2irrap  12180  dfphi2  12220  phiprmpw  12222  crth  12224  phimullem  12225  eulerthlemfi  12228  hashgcdeq  12239  phisum  12240  pceu  12295  pcdiv  12302  pc0  12304  pcqdiv  12307  pcexp  12309  pcxnn0cl  12310  pcxcl  12311  pcdvdstr  12326  dvdsprmpweqnn  12335  pcaddlem  12338  pcadd  12339  pcfaclem  12347  qexpz  12350  zgz  12371  igz  12372  ennnfonelemjn  12403  ennnfonelem1  12408  mulg0  12988  subgmulg  13048  zring0  13493  rpcxp0  14322  lgslem2  14405  lgsfcl2  14410  lgs0  14417  lgsneg  14428  lgsdilem  14431  lgsdir2lem3  14434  lgsdir  14439  lgsdilem2  14440  lgsdi  14441  lgsne0  14442  lgsprme0  14446  lgsdirnn0  14451  lgsdinn0  14452  apdifflemr  14798  apdiff  14799  iswomni0  14802  nconstwlpolem  14815