Theorem 0z 8761

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 7488	. 2 |- 0 e. RR
2		eqid 2088	. . 3 |- 0 = 0
3	2	3mix1i 1115	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 8752	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 888	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 923   = wceq 1289   e. wcel 1438   RRcr 7349   0cc0 7350   -ucneg 7654   NNcn 8422   ZZcz 8750

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-1re 7439  ax-addrcl 7442  ax-rnegex 7454

This theorem depends on definitions:  df-bi 115  df-3or 925  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-rab 2368  df-v 2621  df-un 3003  df-sn 3452  df-pr 3453  df-op 3455  df-uni 3654  df-br 3846  df-iota 4980  df-fv 5023  df-ov 5655  df-neg 7656  df-z 8751

This theorem is referenced by:  0zd  8762  nn0ssz  8768  znegcl  8781  zgt0ge1  8808  nn0n0n1ge2b  8826  nn0lt10b  8827  nnm1ge0  8832  gtndiv  8841  msqznn  8846  zeo  8851  nn0ind  8860  fnn0ind  8862  nn0uz  9053  1eluzge0  9062  eqreznegel  9099  qreccl  9127  qdivcl  9128  irrmul  9132  fz10  9460  fz01en  9467  fzpreddisj  9485  fzshftral  9522  fznn0  9527  fz1ssfz0  9531  fz0tp  9535  elfz0ubfz0  9536  1fv  9550  lbfzo0  9592  elfzonlteqm1  9621  fzo01  9627  fzo0to2pr  9629  fzo0to3tp  9630  flqge0nn0  9700  divfl0  9703  btwnzge0  9707  modqmulnn  9749  zmodfz  9753  modqid  9756  zmodid2  9759  q0mod  9762  modqmuladdnn0  9775  frecfzennn  9833  qexpclz  9976  facdiv  10146  bcval  10157  bcnn  10165  bcm1k  10168  ibcval5  10171  bcpasc  10174  4bc2eq6  10182  hashinfom  10186  rexfiuz  10422  qabsor  10508  nn0abscl  10518  nnabscl  10533  climz  10680  climaddc1  10717  climmulc2  10719  climsubc1  10720  climsubc2  10721  climlec2  10730  binomlem  10877  binom  10878  bcxmas  10883  arisum2  10893  explecnv  10899  ef0lem  10950  dvdsval2  11077  dvdsdc  11082  moddvds  11083  dvds0  11089  0dvds  11094  zdvdsdc  11095  dvdscmulr  11103  dvdsmulcr  11104  dvdslelemd  11122  dvdsabseq  11126  divconjdvds  11128  alzdvds  11133  fzo0dvdseq  11136  odd2np1lem  11150  gcdmndc  11218  gcdsupex  11227  gcdsupcl  11228  gcd0val  11230  gcddvds  11233  gcd0id  11248  gcdid0  11249  gcdid  11255  bezoutlema  11266  bezoutlemb  11267  bezoutlembi  11272  dfgcd3  11277  dfgcd2  11281  gcdmultiplez  11288  dvdssq  11298  algcvgblem  11309  lcmmndc  11322  lcm0val  11325  dvdslcm  11329  lcmeq0  11331  lcmgcd  11338  lcmdvds  11339  lcmid  11340  3lcm2e6woprm  11346  6lcm4e12  11347  cncongr2  11364  sqrt2irrap  11436  dfphi2  11474  phiprmpw  11476  crth  11478  phimullem  11479  hashgcdeq  11482