Theorem 0z 8969

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 7690	. 2 |- 0 e. RR
2		eqid 2115	. . 3 |- 0 = 0
3	2	3mix1i 1136	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 8960	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 909	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 944   = wceq 1314   e. wcel 1463   RRcr 7546   0cc0 7547   -ucneg 7857   NNcn 8630   ZZcz 8958

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-1re 7639  ax-addrcl 7642  ax-rnegex 7654

This theorem depends on definitions:  df-bi 116  df-3or 946  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-ral 2395  df-rex 2396  df-rab 2399  df-v 2659  df-un 3041  df-sn 3499  df-pr 3500  df-op 3502  df-uni 3703  df-br 3896  df-iota 5046  df-fv 5089  df-ov 5731  df-neg 7859  df-z 8959

This theorem is referenced by:  0zd  8970  nn0ssz  8976  znegcl  8989  zgt0ge1  9016  nn0n0n1ge2b  9034  nn0lt10b  9035  nnm1ge0  9041  gtndiv  9050  msqznn  9055  zeo  9060  nn0ind  9069  fnn0ind  9071  nn0uz  9262  1eluzge0  9271  eqreznegel  9308  qreccl  9336  qdivcl  9337  irrmul  9341  fz10  9719  fz01en  9726  fzpreddisj  9744  fzshftral  9781  fznn0  9786  fz1ssfz0  9790  fz0tp  9794  elfz0ubfz0  9795  1fv  9809  lbfzo0  9851  elfzonlteqm1  9880  fzo01  9886  fzo0to2pr  9888  fzo0to3tp  9889  flqge0nn0  9959  divfl0  9962  btwnzge0  9966  modqmulnn  10008  zmodfz  10012  modqid  10015  zmodid2  10018  q0mod  10021  modqmuladdnn0  10034  frecfzennn  10092  qexpclz  10207  facdiv  10377  bcval  10388  bcnn  10396  bcm1k  10399  bcval5  10402  bcpasc  10405  4bc2eq6  10413  hashinfom  10417  rexfiuz  10653  qabsor  10739  nn0abscl  10749  nnabscl  10764  climz  10953  climaddc1  10990  climmulc2  10992  climsubc1  10993  climsubc2  10994  climlec2  11002  binomlem  11144  binom  11145  bcxmas  11150  arisum2  11160  explecnv  11166  ef0lem  11217  dvdsval2  11344  dvdsdc  11349  moddvds  11350  dvds0  11356  0dvds  11361  zdvdsdc  11362  dvdscmulr  11370  dvdsmulcr  11371  dvdslelemd  11389  dvdsabseq  11393  divconjdvds  11395  alzdvds  11400  fzo0dvdseq  11403  odd2np1lem  11417  gcdmndc  11485  gcdsupex  11494  gcdsupcl  11495  gcd0val  11497  gcddvds  11500  gcd0id  11515  gcdid0  11516  gcdid  11522  bezoutlema  11533  bezoutlemb  11534  bezoutlembi  11539  dfgcd3  11544  dfgcd2  11548  gcdmultiplez  11555  dvdssq  11565  algcvgblem  11576  lcmmndc  11589  lcm0val  11592  dvdslcm  11596  lcmeq0  11598  lcmgcd  11605  lcmdvds  11606  lcmid  11607  3lcm2e6woprm  11613  6lcm4e12  11614  cncongr2  11631  sqrt2irrap  11703  dfphi2  11741  phiprmpw  11743  crth  11745  phimullem  11746  hashgcdeq  11749  ennnfonelemjn  11760  ennnfonelem1  11765