Theorem 0z 9664

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 9655	. 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 9653

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 9654

This theorem is used by:  0zd  9665  nn0ssz  9671  znegcl  9684  nnnle0  9702  zgt0ge1  9712  nn0n0n1ge2b  9734  nn0lt10b  9735  nnm1ge0  9741  gtndiv  9751  msqznn  9756  zeo  9761  nn0ind  9770  fnn0ind  9772  nn0uz  9972  1eluzge0  9989  elnn0dc  10026  eqreznegel  10029  qreccl  10057  qdivcl  10058  irrmul  10063  irrmulap  10064  fz10  10466  fz00m1  10467  fz01en  10475  fzpreddisj  10494  fzshftral  10531  fznn0  10536  fz1ssfz0  10540  fz0sn  10544  fz0tp  10545  fz0to3un2pr  10546  fz0to4untppr  10547  elfz0ubfz0  10548  1fv  10562  fzo0n  10591  lbfzo0  10608  elfzonlteqm1  10644  fzo01  10650  fzo0to2pr  10652  fzo0to3tp  10653  flqge0nn0  10748  divfl0  10751  btwnzge0  10755  modqmulnn  10799  zmodfz  10803  modqid  10806  zmodid2  10809  q0mod  10812  modqmuladdnn0  10825  frecfzennn  10883  xnn0nnen  10894  qexpclz  11017  qsqeqor  11107  facdiv  11197  bcval  11208  bcnn  11216  bcm1k  11219  bcval5  11222  bcpasc  11225  4bc2eq6  11234  hashinfom  11238  hashfibc  11304  iswrd  11327  iswrdiz  11332  wrdexg  11336  wrdfin  11344  wrdnval  11356  wrdred1hash  11369  lsw0  11373  ccatsymb  11391  ccatalpha  11402  s111  11420  ccat1st1st  11430  fzowrddc  11440  swrdlen  11445  swrdnd  11452  swrdwrdsymbg  11457  swrds1  11461  pfxval  11467  pfx00g  11468  pfx0g  11469  fnpfx  11470  pfxlen  11478  swrdccatin1  11518  swrdccat  11528  swrdccat3blem  11532  rexfiuz  11776  qabsor  11862  nn0abscl  11873  nnabscl  11888  climz  12082  climaddc1  12119  climmulc2  12121  climsubc1  12122  climsubc2  12123  climlec2  12131  binomlem  12274  binom  12275  bcxmas  12280  arisum2  12290  explecnv  12296  ef0lem  12451  dvdsval2  12581  dvdsdc  12589  moddvds  12590  dvds0  12597  0dvds  12602  zdvdsdc  12603  dvdscmulr  12611  dvdsmulcr  12612  fsumdvds  12633  dvdslelemd  12634  dvdsabseq  12638  divconjdvds  12640  alzdvds  12645  fzo0dvdseq  12648  odd2np1lem  12663  bitsfzo  12746  bitsmod  12747  0bits  12750  m1bits  12751  bitsinv1lem  12752  bitsinv1  12753  gcdmndc  12756  gcdsupex  12758  gcdsupcl  12759  gcd0val  12761  gcddvds  12764  gcd0id  12780  gcdid0  12781  gcdid  12787  bezoutlema  12800  bezoutlemb  12801  bezoutlembi  12806  dfgcd3  12811  dfgcd2  12815  gcdmultiplez  12822  dvdssq  12832  algcvgblem  12851  lcmmndc  12864  lcm0val  12867  dvdslcm  12871  lcmeq0  12873  lcmgcd  12880  lcmdvds  12881  lcmid  12882  3lcm2e6woprm  12888  6lcm4e12  12889  cncongr2  12906  sqrt2irrap  12984  sqrtrirr  13013  dfphi2  13026  phiprmpw  13028  crth  13030  phimullem  13031  eulerthlemfi  13034  hashgcdeq  13046  phisum  13047  pceu  13102  pcdiv  13109  pc0  13111  pcqdiv  13114  pcexp  13116  pcxnn0cl  13117  pcxcl  13118  pcxqcl  13119  pcdvdstr  13134  dvdsprmpweqnn  13143  pcaddlem  13146  pcadd  13147  pcfaclem  13156  qexpz  13159  zgz  13180  igz  13181  4sqlem19  13216  1259lem1  13270  1259lem4  13273  ballotfilemonn  13278  ballotfilem2  13285  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemefi  13294  ballotfilemodife  13297  ballotfilemscl  13304  ballotfilemsle  13305  ennnfonelemjn  13350  ennnfonelem1  13355  mulg0  13986  subgmulg  14049  zring0  15043  zndvds0  15093  znf1o  15094  znfi  15098  znhash  15099  psr1clfi  15207  plycolemc  16001  rpcxp0  16148  0sgm  16271  ppiqltx  16298  1sgmprm  16305  ppiqub  16310  bcmono  16321  bposlem1  16328  bposlem2  16329  lgslem2  16342  lgsfcl2  16347  lgs0  16354  lgsneg  16365  lgsdilem  16368  lgsdir2lem3  16371  lgsdir  16376  lgsdilem2  16377  lgsdi  16378  lgsne0  16379  lgsprme0  16383  lgsdirnn0  16388  lgsdinn0  16389  usgrexmpldifpr  16712  vdegp1bid  16778  wlkv0  16832  wlklenvclwlk  16836  upgr2wlkdc  16840  clwwlkccatlem  16863  eupthfi  16914  trlsegvdeglem6  16928  konigsbergvtx  16945  konigsbergiedg  16946  konigsbergumgr  16950  konigsberglem1  16951  konigsberglem2  16952  konigsberglem3  16953  konigsberglem5  16955  konigsberg  16956  apdifflemr  17320  apdiff  17321  qdiff  17322  iswomni0  17325  nconstwlpolem  17339