Theorem 0z 9660

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 8327	. 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 9651	. 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 8179   0cc0 8180   -ucneg 8500   NNcn 9307   ZZcz 9649

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 8274  ax-addrcl 8277  ax-rnegex 8289

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 8502  df-z 9650

This theorem is used by:  0zd  9661  nn0ssz  9667  znegcl  9680  nnnle0  9698  zgt0ge1  9708  nn0n0n1ge2b  9730  nn0lt10b  9731  nnm1ge0  9737  gtndiv  9746  msqznn  9751  zeo  9756  nn0ind  9765  fnn0ind  9767  nn0uz  9967  1eluzge0  9984  elnn0dc  10021  eqreznegel  10024  qreccl  10052  qdivcl  10053  irrmul  10058  irrmulap  10059  fz10  10461  fz00m1  10462  fz01en  10470  fzpreddisj  10489  fzshftral  10526  fznn0  10531  fz1ssfz0  10535  fz0sn  10539  fz0tp  10540  fz0to3un2pr  10541  fz0to4untppr  10542  elfz0ubfz0  10543  1fv  10557  fzo0n  10586  lbfzo0  10603  elfzonlteqm1  10639  fzo01  10645  fzo0to2pr  10647  fzo0to3tp  10648  flqge0nn0  10743  divfl0  10746  btwnzge0  10750  modqmulnn  10794  zmodfz  10798  modqid  10801  zmodid2  10804  q0mod  10807  modqmuladdnn0  10820  frecfzennn  10878  xnn0nnen  10889  qexpclz  11012  qsqeqor  11102  facdiv  11192  bcval  11203  bcnn  11211  bcm1k  11214  bcval5  11217  bcpasc  11220  4bc2eq6  11229  hashinfom  11233  hashfibc  11299  iswrd  11322  iswrdiz  11327  wrdexg  11331  wrdfin  11339  wrdnval  11351  wrdred1hash  11364  lsw0  11368  ccatsymb  11386  ccatalpha  11397  s111  11415  ccat1st1st  11425  fzowrddc  11435  swrdlen  11440  swrdnd  11447  swrdwrdsymbg  11452  swrds1  11456  pfxval  11462  pfx00g  11463  pfx0g  11464  fnpfx  11465  pfxlen  11473  swrdccatin1  11513  swrdccat  11523  swrdccat3blem  11527  rexfiuz  11771  qabsor  11857  nn0abscl  11868  nnabscl  11883  climz  12077  climaddc1  12114  climmulc2  12116  climsubc1  12117  climsubc2  12118  climlec2  12126  binomlem  12269  binom  12270  bcxmas  12275  arisum2  12285  explecnv  12291  ef0lem  12446  dvdsval2  12576  dvdsdc  12584  moddvds  12585  dvds0  12592  0dvds  12597  zdvdsdc  12598  dvdscmulr  12606  dvdsmulcr  12607  fsumdvds  12628  dvdslelemd  12629  dvdsabseq  12633  divconjdvds  12635  alzdvds  12640  fzo0dvdseq  12643  odd2np1lem  12658  bitsfzo  12741  bitsmod  12742  0bits  12745  m1bits  12746  bitsinv1lem  12747  bitsinv1  12748  gcdmndc  12751  gcdsupex  12753  gcdsupcl  12754  gcd0val  12756  gcddvds  12759  gcd0id  12775  gcdid0  12776  gcdid  12782  bezoutlema  12795  bezoutlemb  12796  bezoutlembi  12801  dfgcd3  12806  dfgcd2  12810  gcdmultiplez  12817  dvdssq  12827  algcvgblem  12846  lcmmndc  12859  lcm0val  12862  dvdslcm  12866  lcmeq0  12868  lcmgcd  12875  lcmdvds  12876  lcmid  12877  3lcm2e6woprm  12883  6lcm4e12  12884  cncongr2  12901  sqrt2irrap  12979  sqrtrirr  13008  dfphi2  13021  phiprmpw  13023  crth  13025  phimullem  13026  eulerthlemfi  13029  hashgcdeq  13041  phisum  13042  pceu  13097  pcdiv  13104  pc0  13106  pcqdiv  13109  pcexp  13111  pcxnn0cl  13112  pcxcl  13113  pcxqcl  13114  pcdvdstr  13129  dvdsprmpweqnn  13138  pcaddlem  13141  pcadd  13142  pcfaclem  13151  qexpz  13154  zgz  13175  igz  13176  4sqlem19  13211  1259lem1  13265  1259lem4  13268  ballotfilemonn  13273  ballotfilem2  13280  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemefi  13289  ballotfilemodife  13292  ballotfilemscl  13299  ballotfilemsle  13300  ennnfonelemjn  13345  ennnfonelem1  13350  mulg0  13981  subgmulg  14044  zring0  15019  zndvds0  15069  znf1o  15070  znfi  15074  znhash  15075  psr1clfi  15170  plycolemc  15950  rpcxp0  16095  0sgm  16215  ppiqltx  16242  1sgmprm  16249  ppiqub  16254  bcmono  16265  bposlem1  16272  bposlem2  16273  lgslem2  16286  lgsfcl2  16291  lgs0  16298  lgsneg  16309  lgsdilem  16312  lgsdir2lem3  16315  lgsdir  16320  lgsdilem2  16321  lgsdi  16322  lgsne0  16323  lgsprme0  16327  lgsdirnn0  16332  lgsdinn0  16333  usgrexmpldifpr  16656  vdegp1bid  16722  wlkv0  16776  wlklenvclwlk  16780  upgr2wlkdc  16784  clwwlkccatlem  16807  eupthfi  16858  trlsegvdeglem6  16872  konigsbergvtx  16889  konigsbergiedg  16890  konigsbergumgr  16894  konigsberglem1  16895  konigsberglem2  16896  konigsberglem3  16897  konigsberglem5  16899  konigsberg  16900  apdifflemr  17263  apdiff  17264  qdiff  17265  iswomni0  17268  nconstwlpolem  17282