Theorem 0z 9659

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 8326	. 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 9650	. 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 8178   0cc0 8179   -ucneg 8499   NNcn 9306   ZZcz 9648

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 8273  ax-addrcl 8276  ax-rnegex 8288

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 4131  df-iota 5337  df-fv 5385  df-ov 6088  df-neg 8501  df-z 9649

This theorem is used by:  0zd  9660  nn0ssz  9666  znegcl  9679  nnnle0  9697  zgt0ge1  9707  nn0n0n1ge2b  9729  nn0lt10b  9730  nnm1ge0  9736  gtndiv  9745  msqznn  9750  zeo  9755  nn0ind  9764  fnn0ind  9766  nn0uz  9966  1eluzge0  9983  elnn0dc  10020  eqreznegel  10023  qreccl  10051  qdivcl  10052  irrmul  10057  irrmulap  10058  fz10  10460  fz00m1  10461  fz01en  10469  fzpreddisj  10488  fzshftral  10525  fznn0  10530  fz1ssfz0  10534  fz0sn  10538  fz0tp  10539  fz0to3un2pr  10540  fz0to4untppr  10541  elfz0ubfz0  10542  1fv  10556  fzo0n  10585  lbfzo0  10602  elfzonlteqm1  10638  fzo01  10644  fzo0to2pr  10646  fzo0to3tp  10647  flqge0nn0  10741  divfl0  10744  btwnzge0  10748  modqmulnn  10792  zmodfz  10796  modqid  10799  zmodid2  10802  q0mod  10805  modqmuladdnn0  10818  frecfzennn  10876  xnn0nnen  10887  qexpclz  11010  qsqeqor  11100  facdiv  11190  bcval  11201  bcnn  11209  bcm1k  11212  bcval5  11215  bcpasc  11218  4bc2eq6  11227  hashinfom  11231  hashfibc  11297  iswrd  11320  iswrdiz  11325  wrdexg  11329  wrdfin  11337  wrdnval  11349  wrdred1hash  11362  lsw0  11366  ccatsymb  11384  ccatalpha  11395  s111  11413  ccat1st1st  11423  fzowrddc  11433  swrdlen  11438  swrdnd  11445  swrdwrdsymbg  11450  swrds1  11454  pfxval  11460  pfx00g  11461  pfx0g  11462  fnpfx  11463  pfxlen  11471  swrdccatin1  11511  swrdccat  11521  swrdccat3blem  11525  rexfiuz  11769  qabsor  11855  nn0abscl  11866  nnabscl  11881  climz  12074  climaddc1  12111  climmulc2  12113  climsubc1  12114  climsubc2  12115  climlec2  12123  binomlem  12266  binom  12267  bcxmas  12272  arisum2  12282  explecnv  12288  ef0lem  12443  dvdsval2  12573  dvdsdc  12581  moddvds  12582  dvds0  12589  0dvds  12594  zdvdsdc  12595  dvdscmulr  12603  dvdsmulcr  12604  fsumdvds  12625  dvdslelemd  12626  dvdsabseq  12630  divconjdvds  12632  alzdvds  12637  fzo0dvdseq  12640  odd2np1lem  12655  bitsfzo  12738  bitsmod  12739  0bits  12742  m1bits  12743  bitsinv1lem  12744  bitsinv1  12745  gcdmndc  12748  gcdsupex  12750  gcdsupcl  12751  gcd0val  12753  gcddvds  12756  gcd0id  12772  gcdid0  12773  gcdid  12779  bezoutlema  12792  bezoutlemb  12793  bezoutlembi  12798  dfgcd3  12803  dfgcd2  12807  gcdmultiplez  12814  dvdssq  12824  algcvgblem  12843  lcmmndc  12856  lcm0val  12859  dvdslcm  12863  lcmeq0  12865  lcmgcd  12872  lcmdvds  12873  lcmid  12874  3lcm2e6woprm  12880  6lcm4e12  12881  cncongr2  12898  sqrt2irrap  12976  sqrtrirr  13005  dfphi2  13018  phiprmpw  13020  crth  13022  phimullem  13023  eulerthlemfi  13026  hashgcdeq  13038  phisum  13039  pceu  13094  pcdiv  13101  pc0  13103  pcqdiv  13106  pcexp  13108  pcxnn0cl  13109  pcxcl  13110  pcxqcl  13111  pcdvdstr  13126  dvdsprmpweqnn  13135  pcaddlem  13138  pcadd  13139  pcfaclem  13148  qexpz  13151  zgz  13172  igz  13173  4sqlem19  13208  1259lem1  13262  1259lem4  13265  ballotfilemonn  13270  ballotfilem2  13277  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemefi  13286  ballotfilemodife  13289  ballotfilemscl  13296  ballotfilemsle  13297  ennnfonelemjn  13342  ennnfonelem1  13347  mulg0  13977  subgmulg  14040  zring0  14984  zndvds0  15034  znf1o  15035  znfi  15039  znhash  15040  psr1clfi  15128  plycolemc  15908  rpcxp0  16053  0sgm  16166  ppiqltx  16183  1sgmprm  16189  ppiqub  16194  bcmono  16202  bposlem1  16209  bposlem2  16210  lgslem2  16218  lgsfcl2  16223  lgs0  16230  lgsneg  16241  lgsdilem  16244  lgsdir2lem3  16247  lgsdir  16252  lgsdilem2  16253  lgsdi  16254  lgsne0  16255  lgsprme0  16259  lgsdirnn0  16264  lgsdinn0  16265  usgrexmpldifpr  16588  vdegp1bid  16654  wlkv0  16708  wlklenvclwlk  16712  upgr2wlkdc  16716  clwwlkccatlem  16739  eupthfi  16790  trlsegvdeglem6  16804  konigsbergvtx  16821  konigsbergiedg  16822  konigsbergumgr  16826  konigsberglem1  16827  konigsberglem2  16828  konigsberglem3  16829  konigsberglem5  16831  konigsberg  16832  apdifflemr  17194  apdiff  17195  qdiff  17196  iswomni0  17199  nconstwlpolem  17213