Theorem 0z 9223

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 7920	. 2 |- 0 e. RR
2		eqid 2170	. . 3 |- 0 = 0
3	2	3mix1i 1164	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9214	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 937	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 972   = wceq 1348   e. wcel 2141   RRcr 7773   0cc0 7774   -ucneg 8091   NNcn 8878   ZZcz 9212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-1re 7868  ax-addrcl 7871  ax-rnegex 7883

This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-rab 2457  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-iota 5160  df-fv 5206  df-ov 5856  df-neg 8093  df-z 9213

This theorem is referenced by:  0zd  9224  nn0ssz  9230  znegcl  9243  zgt0ge1  9270  nn0n0n1ge2b  9291  nn0lt10b  9292  nnm1ge0  9298  gtndiv  9307  msqznn  9312  zeo  9317  nn0ind  9326  fnn0ind  9328  nn0uz  9521  1eluzge0  9533  elnn0dc  9570  eqreznegel  9573  qreccl  9601  qdivcl  9602  irrmul  9606  fz10  10002  fz01en  10009  fzpreddisj  10027  fzshftral  10064  fznn0  10069  fz1ssfz0  10073  fz0sn  10077  fz0tp  10078  fz0to3un2pr  10079  fz0to4untppr  10080  elfz0ubfz0  10081  1fv  10095  lbfzo0  10137  elfzonlteqm1  10166  fzo01  10172  fzo0to2pr  10174  fzo0to3tp  10175  flqge0nn0  10249  divfl0  10252  btwnzge0  10256  modqmulnn  10298  zmodfz  10302  modqid  10305  zmodid2  10308  q0mod  10311  modqmuladdnn0  10324  frecfzennn  10382  qexpclz  10497  qsqeqor  10586  facdiv  10672  bcval  10683  bcnn  10691  bcm1k  10694  bcval5  10697  bcpasc  10700  4bc2eq6  10708  hashinfom  10712  rexfiuz  10953  qabsor  11039  nn0abscl  11049  nnabscl  11064  climz  11255  climaddc1  11292  climmulc2  11294  climsubc1  11295  climsubc2  11296  climlec2  11304  binomlem  11446  binom  11447  bcxmas  11452  arisum2  11462  explecnv  11468  ef0lem  11623  dvdsval2  11752  dvdsdc  11760  moddvds  11761  dvds0  11768  0dvds  11773  zdvdsdc  11774  dvdscmulr  11782  dvdsmulcr  11783  dvdslelemd  11803  dvdsabseq  11807  divconjdvds  11809  alzdvds  11814  fzo0dvdseq  11817  odd2np1lem  11831  gcdmndc  11899  gcdsupex  11912  gcdsupcl  11913  gcd0val  11915  gcddvds  11918  gcd0id  11934  gcdid0  11935  gcdid  11941  bezoutlema  11954  bezoutlemb  11955  bezoutlembi  11960  dfgcd3  11965  dfgcd2  11969  gcdmultiplez  11976  dvdssq  11986  algcvgblem  12003  lcmmndc  12016  lcm0val  12019  dvdslcm  12023  lcmeq0  12025  lcmgcd  12032  lcmdvds  12033  lcmid  12034  3lcm2e6woprm  12040  6lcm4e12  12041  cncongr2  12058  sqrt2irrap  12134  dfphi2  12174  phiprmpw  12176  crth  12178  phimullem  12179  eulerthlemfi  12182  hashgcdeq  12193  phisum  12194  pceu  12249  pcdiv  12256  pc0  12258  pcqdiv  12261  pcexp  12263  pcxnn0cl  12264  pcxcl  12265  pcdvdstr  12280  dvdsprmpweqnn  12289  pcaddlem  12292  pcadd  12293  pcfaclem  12301  qexpz  12304  zgz  12325  igz  12326  ennnfonelemjn  12357  ennnfonelem1  12362  rpcxp0  13613  lgslem2  13696  lgsfcl2  13701  lgs0  13708  lgsneg  13719  lgsdilem  13722  lgsdir2lem3  13725  lgsdir  13730  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  lgsprme0  13737  lgsdirnn0  13742  lgsdinn0  13743  apdifflemr  14079  apdiff  14080  iswomni0  14083  nconstwlpolem  14096