Theorem 0z 9237

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 7932	. 2 |- 0 e. RR
2		eqid 2175	. . 3 |- 0 = 0
3	2	3mix1i 1169	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9228	. 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 2146   RRcr 7785   0cc0 7786   -ucneg 8103   NNcn 8892   ZZcz 9226

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-1re 7880  ax-addrcl 7883  ax-rnegex 7895

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-rex 2459  df-rab 2462  df-v 2737  df-un 3131  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-br 3999  df-iota 5170  df-fv 5216  df-ov 5868  df-neg 8105  df-z 9227

This theorem is referenced by:  0zd  9238  nn0ssz  9244  znegcl  9257  zgt0ge1  9284  nn0n0n1ge2b  9305  nn0lt10b  9306  nnm1ge0  9312  gtndiv  9321  msqznn  9326  zeo  9331  nn0ind  9340  fnn0ind  9342  nn0uz  9535  1eluzge0  9547  elnn0dc  9584  eqreznegel  9587  qreccl  9615  qdivcl  9616  irrmul  9620  fz10  10016  fz01en  10023  fzpreddisj  10041  fzshftral  10078  fznn0  10083  fz1ssfz0  10087  fz0sn  10091  fz0tp  10092  fz0to3un2pr  10093  fz0to4untppr  10094  elfz0ubfz0  10095  1fv  10109  lbfzo0  10151  elfzonlteqm1  10180  fzo01  10186  fzo0to2pr  10188  fzo0to3tp  10189  flqge0nn0  10263  divfl0  10266  btwnzge0  10270  modqmulnn  10312  zmodfz  10316  modqid  10319  zmodid2  10322  q0mod  10325  modqmuladdnn0  10338  frecfzennn  10396  qexpclz  10511  qsqeqor  10600  facdiv  10686  bcval  10697  bcnn  10705  bcm1k  10708  bcval5  10711  bcpasc  10714  4bc2eq6  10722  hashinfom  10726  rexfiuz  10966  qabsor  11052  nn0abscl  11062  nnabscl  11077  climz  11268  climaddc1  11305  climmulc2  11307  climsubc1  11308  climsubc2  11309  climlec2  11317  binomlem  11459  binom  11460  bcxmas  11465  arisum2  11475  explecnv  11481  ef0lem  11636  dvdsval2  11765  dvdsdc  11773  moddvds  11774  dvds0  11781  0dvds  11786  zdvdsdc  11787  dvdscmulr  11795  dvdsmulcr  11796  dvdslelemd  11816  dvdsabseq  11820  divconjdvds  11822  alzdvds  11827  fzo0dvdseq  11830  odd2np1lem  11844  gcdmndc  11912  gcdsupex  11925  gcdsupcl  11926  gcd0val  11928  gcddvds  11931  gcd0id  11947  gcdid0  11948  gcdid  11954  bezoutlema  11967  bezoutlemb  11968  bezoutlembi  11973  dfgcd3  11978  dfgcd2  11982  gcdmultiplez  11989  dvdssq  11999  algcvgblem  12016  lcmmndc  12029  lcm0val  12032  dvdslcm  12036  lcmeq0  12038  lcmgcd  12045  lcmdvds  12046  lcmid  12047  3lcm2e6woprm  12053  6lcm4e12  12054  cncongr2  12071  sqrt2irrap  12147  dfphi2  12187  phiprmpw  12189  crth  12191  phimullem  12192  eulerthlemfi  12195  hashgcdeq  12206  phisum  12207  pceu  12262  pcdiv  12269  pc0  12271  pcqdiv  12274  pcexp  12276  pcxnn0cl  12277  pcxcl  12278  pcdvdstr  12293  dvdsprmpweqnn  12302  pcaddlem  12305  pcadd  12306  pcfaclem  12314  qexpz  12317  zgz  12338  igz  12339  ennnfonelemjn  12370  ennnfonelem1  12375  mulg0  12849  rpcxp0  13890  lgslem2  13973  lgsfcl2  13978  lgs0  13985  lgsneg  13996  lgsdilem  13999  lgsdir2lem3  14002  lgsdir  14007  lgsdilem2  14008  lgsdi  14009  lgsne0  14010  lgsprme0  14014  lgsdirnn0  14019  lgsdinn0  14020  apdifflemr  14356  apdiff  14357  iswomni0  14360  nconstwlpolem  14373