Theorem 0z 9666

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 8332	. 2 |- 0 e. RR
2		eqid 2238	. . 3 |- 0 = 0
3	2	3mix1i 1200	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9657	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 955	1 |- 0 e. ZZ

This proof depends on syntax axioms:   \/ w3o 1008   = wceq 1402   e. wcel 2209   RRcr 8184   0cc0 8185   -ucneg 8505   NNcn 9313   ZZcz 9655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1re 8279  ax-addrcl 8282  ax-rnegex 8294

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-rab 2537  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388  df-ov 6091  df-neg 8507  df-z 9656

This theorem is used by:  0zd  9667  nn0ssz  9673  znegcl  9686  nnnle0  9704  zgt0ge1  9714  nn0n0n1ge2b  9736  nn0lt10b  9737  nnm1ge0  9743  gtndiv  9752  msqznn  9757  zeo  9762  nn0ind  9771  fnn0ind  9773  nn0uz  9973  1eluzge0  9990  elnn0dc  10027  eqreznegel  10030  qreccl  10058  qdivcl  10059  irrmul  10064  irrmulap  10065  fz10  10467  fz00m1  10468  fz01en  10476  fzpreddisj  10495  fzshftral  10532  fznn0  10537  fz1ssfz0  10541  fz0sn  10545  fz0tp  10546  fz0to3un2pr  10547  fz0to4untppr  10548  elfz0ubfz0  10549  1fv  10563  fzo0n  10592  lbfzo0  10609  elfzonlteqm1  10645  fzo01  10651  fzo0to2pr  10653  fzo0to3tp  10654  flqge0nn0  10749  divfl0  10752  btwnzge0  10756  modqmulnn  10800  zmodfz  10804  modqid  10807  zmodid2  10810  q0mod  10813  modqmuladdnn0  10826  frecfzennn  10884  xnn0nnen  10895  qexpclz  11018  qsqeqor  11108  facdiv  11198  bcval  11209  bcnn  11217  bcm1k  11220  bcval5  11223  bcpasc  11226  4bc2eq6  11235  hashinfom  11239  hashfibc  11305  iswrd  11328  iswrdiz  11333  wrdexg  11337  wrdfin  11345  wrdnval  11357  wrdred1hash  11370  lsw0  11374  ccatsymb  11392  ccatalpha  11403  s111  11421  ccat1st1st  11431  fzowrddc  11441  swrdlen  11446  swrdnd  11453  swrdwrdsymbg  11458  swrds1  11462  pfxval  11468  pfx00g  11469  pfx0g  11470  fnpfx  11471  pfxlen  11479  swrdccatin1  11519  swrdccat  11529  swrdccat3blem  11533  rexfiuz  11777  qabsor  11863  nn0abscl  11874  nnabscl  11889  climz  12083  climaddc1  12120  climmulc2  12122  climsubc1  12123  climsubc2  12124  climlec2  12132  binomlem  12275  binom  12276  bcxmas  12281  arisum2  12291  explecnv  12297  ef0lem  12452  dvdsval2  12582  dvdsdc  12590  moddvds  12591  dvds0  12598  0dvds  12603  zdvdsdc  12604  dvdscmulr  12612  dvdsmulcr  12613  fsumdvds  12634  dvdslelemd  12635  dvdsabseq  12639  divconjdvds  12641  alzdvds  12646  fzo0dvdseq  12649  odd2np1lem  12664  bitsfzo  12747  bitsmod  12748  0bits  12751  m1bits  12752  bitsinv1lem  12753  bitsinv1  12754  gcdmndc  12757  gcdsupex  12759  gcdsupcl  12760  gcd0val  12762  gcddvds  12765  gcd0id  12781  gcdid0  12782  gcdid  12788  bezoutlema  12801  bezoutlemb  12802  bezoutlembi  12807  dfgcd3  12812  dfgcd2  12816  gcdmultiplez  12823  dvdssq  12833  algcvgblem  12852  lcmmndc  12865  lcm0val  12868  dvdslcm  12872  lcmeq0  12874  lcmgcd  12881  lcmdvds  12882  lcmid  12883  3lcm2e6woprm  12889  6lcm4e12  12890  cncongr2  12907  sqrt2irrap  12985  sqrtrirr  13014  dfphi2  13027  phiprmpw  13029  crth  13031  phimullem  13032  eulerthlemfi  13035  hashgcdeq  13047  phisum  13048  pceu  13103  pcdiv  13110  pc0  13112  pcqdiv  13115  pcexp  13117  pcxnn0cl  13118  pcxcl  13119  pcxqcl  13120  pcdvdstr  13135  dvdsprmpweqnn  13144  pcaddlem  13147  pcadd  13148  pcfaclem  13157  qexpz  13160  zgz  13181  igz  13182  4sqlem19  13217  1259lem1  13271  1259lem4  13274  ballotfilemonn  13279  ballotfilem2  13286  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemefi  13295  ballotfilemodife  13298  ballotfilemscl  13305  ballotfilemsle  13306  ennnfonelemjn  13351  ennnfonelem1  13356  mulg0  13987  subgmulg  14050  zring0  15044  zndvds0  15094  znf1o  15095  znfi  15099  znhash  15100  psr1clfi  15198  plycolemc  15984  rpcxp0  16131  0sgm  16254  ppiqltx  16281  1sgmprm  16288  ppiqub  16293  bcmono  16304  bposlem1  16311  bposlem2  16312  lgslem2  16325  lgsfcl2  16330  lgs0  16337  lgsneg  16348  lgsdilem  16351  lgsdir2lem3  16354  lgsdir  16359  lgsdilem2  16360  lgsdi  16361  lgsne0  16362  lgsprme0  16366  lgsdirnn0  16371  lgsdinn0  16372  usgrexmpldifpr  16695  vdegp1bid  16761  wlkv0  16815  wlklenvclwlk  16819  upgr2wlkdc  16823  clwwlkccatlem  16846  eupthfi  16897  trlsegvdeglem6  16911  konigsbergvtx  16928  konigsbergiedg  16929  konigsbergumgr  16933  konigsberglem1  16934  konigsberglem2  16935  konigsberglem3  16936  konigsberglem5  16938  konigsberg  16939  apdifflemr  17303  apdiff  17304  qdiff  17305  iswomni0  17308  nconstwlpolem  17322