Theorem 0z 9588

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 8274	. 2 |- 0 e. RR
2		eqid 2232	. . 3 |- 0 = 0
3	2	3mix1i 1196	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9579	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 951	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 1004   = wceq 1398   e. wcel 2203   RRcr 8126   0cc0 8127   -ucneg 8445   NNcn 9237   ZZcz 9577

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-1re 8221  ax-addrcl 8224  ax-rnegex 8236

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-rab 2529  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360  df-ov 6053  df-neg 8447  df-z 9578

This theorem is referenced by:  0zd  9589  nn0ssz  9595  znegcl  9608  nnnle0  9626  zgt0ge1  9636  nn0n0n1ge2b  9657  nn0lt10b  9658  nnm1ge0  9664  gtndiv  9673  msqznn  9678  zeo  9683  nn0ind  9692  fnn0ind  9694  nn0uz  9889  1eluzge0  9906  elnn0dc  9943  eqreznegel  9946  qreccl  9974  qdivcl  9975  irrmul  9979  irrmulap  9980  fz10  10380  fz01en  10387  fzpreddisj  10405  fzshftral  10442  fznn0  10447  fz1ssfz0  10451  fz0sn  10455  fz0tp  10456  fz0to3un2pr  10457  fz0to4untppr  10458  elfz0ubfz0  10459  1fv  10473  fzo0n  10502  lbfzo0  10519  elfzonlteqm1  10555  fzo01  10561  fzo0to2pr  10563  fzo0to3tp  10564  flqge0nn0  10653  divfl0  10656  btwnzge0  10660  modqmulnn  10704  zmodfz  10708  modqid  10711  zmodid2  10714  q0mod  10717  modqmuladdnn0  10730  frecfzennn  10788  xnn0nnen  10799  qexpclz  10922  qsqeqor  11012  facdiv  11100  bcval  11111  bcnn  11119  bcm1k  11122  bcval5  11125  bcpasc  11128  4bc2eq6  11137  hashinfom  11141  hashfibc  11207  iswrd  11226  iswrdiz  11231  wrdexg  11235  wrdfin  11243  wrdnval  11255  wrdred1hash  11268  lsw0  11272  ccatsymb  11290  ccatalpha  11301  s111  11319  ccat1st1st  11329  fzowrddc  11339  swrdlen  11344  swrdnd  11351  swrdwrdsymbg  11356  swrds1  11360  pfxval  11366  pfx00g  11367  pfx0g  11368  fnpfx  11369  pfxlen  11377  swrdccatin1  11417  swrdccat  11427  swrdccat3blem  11431  rexfiuz  11674  qabsor  11760  nn0abscl  11770  nnabscl  11785  climz  11977  climaddc1  12014  climmulc2  12016  climsubc1  12017  climsubc2  12018  climlec2  12026  binomlem  12169  binom  12170  bcxmas  12175  arisum2  12185  explecnv  12191  ef0lem  12346  dvdsval2  12476  dvdsdc  12484  moddvds  12485  dvds0  12492  0dvds  12497  zdvdsdc  12498  dvdscmulr  12506  dvdsmulcr  12507  fsumdvds  12528  dvdslelemd  12529  dvdsabseq  12533  divconjdvds  12535  alzdvds  12540  fzo0dvdseq  12543  odd2np1lem  12558  bitsfzo  12641  bitsmod  12642  0bits  12645  m1bits  12646  bitsinv1lem  12647  bitsinv1  12648  gcdmndc  12651  gcdsupex  12653  gcdsupcl  12654  gcd0val  12656  gcddvds  12659  gcd0id  12675  gcdid0  12676  gcdid  12682  bezoutlema  12695  bezoutlemb  12696  bezoutlembi  12701  dfgcd3  12706  dfgcd2  12710  gcdmultiplez  12717  dvdssq  12727  algcvgblem  12746  lcmmndc  12759  lcm0val  12762  dvdslcm  12766  lcmeq0  12768  lcmgcd  12775  lcmdvds  12776  lcmid  12777  3lcm2e6woprm  12783  6lcm4e12  12784  cncongr2  12801  sqrt2irrap  12877  dfphi2  12917  phiprmpw  12919  crth  12921  phimullem  12922  eulerthlemfi  12925  hashgcdeq  12937  phisum  12938  pceu  12993  pcdiv  13000  pc0  13002  pcqdiv  13005  pcexp  13007  pcxnn0cl  13008  pcxcl  13009  pcxqcl  13010  pcdvdstr  13025  dvdsprmpweqnn  13034  pcaddlem  13037  pcadd  13038  pcfaclem  13047  qexpz  13050  zgz  13071  igz  13072  4sqlem19  13107  ballotfilemonn  13140  ballotfilem2  13142  ennnfonelemjn  13153  ennnfonelem1  13158  mulg0  13842  subgmulg  13905  zring0  14748  zndvds0  14798  znf1o  14799  znfi  14803  znhash  14804  psr1clfi  14843  plycolemc  15623  rpcxp0  15763  0sgm  15853  1sgmprm  15862  lgslem2  15874  lgsfcl2  15879  lgs0  15886  lgsneg  15897  lgsdilem  15900  lgsdir2lem3  15903  lgsdir  15908  lgsdilem2  15909  lgsdi  15910  lgsne0  15911  lgsprme0  15915  lgsdirnn0  15920  lgsdinn0  15921  usgrexmpldifpr  16244  vdegp1bid  16310  wlkv0  16364  wlklenvclwlk  16368  upgr2wlkdc  16372  clwwlkccatlem  16395  eupthfi  16446  trlsegvdeglem6  16460  konigsbergvtx  16477  konigsbergiedg  16478  konigsbergumgr  16482  konigsberglem1  16483  konigsberglem2  16484  konigsberglem3  16485  konigsberglem5  16487  konigsberg  16488  apdifflemr  16831  apdiff  16832  qdiff  16833  iswomni0  16836  nconstwlpolem  16851