Theorem 0z 9418

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 8107	. 2 |- 0 e. RR
2		eqid 2207	. . 3 |- 0 = 0
3	2	3mix1i 1172	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9409	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 945	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 980   = wceq 1373   e. wcel 2178   RRcr 7959   0cc0 7960   -ucneg 8279   NNcn 9071   ZZcz 9407

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-1re 8054  ax-addrcl 8057  ax-rnegex 8069

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-rab 2495  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970  df-neg 8281  df-z 9408

This theorem is referenced by:  0zd  9419  nn0ssz  9425  znegcl  9438  nnnle0  9456  zgt0ge1  9466  nn0n0n1ge2b  9487  nn0lt10b  9488  nnm1ge0  9494  gtndiv  9503  msqznn  9508  zeo  9513  nn0ind  9522  fnn0ind  9524  nn0uz  9718  1eluzge0  9730  elnn0dc  9767  eqreznegel  9770  qreccl  9798  qdivcl  9799  irrmul  9803  irrmulap  9804  fz10  10203  fz01en  10210  fzpreddisj  10228  fzshftral  10265  fznn0  10270  fz1ssfz0  10274  fz0sn  10278  fz0tp  10279  fz0to3un2pr  10280  fz0to4untppr  10281  elfz0ubfz0  10282  1fv  10296  fzo0n  10325  lbfzo0  10342  elfzonlteqm1  10376  fzo01  10382  fzo0to2pr  10384  fzo0to3tp  10385  flqge0nn0  10473  divfl0  10476  btwnzge0  10480  modqmulnn  10524  zmodfz  10528  modqid  10531  zmodid2  10534  q0mod  10537  modqmuladdnn0  10550  frecfzennn  10608  xnn0nnen  10619  qexpclz  10742  qsqeqor  10832  facdiv  10920  bcval  10931  bcnn  10939  bcm1k  10942  bcval5  10945  bcpasc  10948  4bc2eq6  10956  hashinfom  10960  iswrd  11033  iswrdiz  11038  wrdexg  11042  wrdfin  11050  wrdnval  11061  wrdred1hash  11074  lsw0  11078  ccatsymb  11096  s111  11123  ccat1st1st  11131  fzowrddc  11138  swrdlen  11143  swrdnd  11150  swrdwrdsymbg  11155  swrds1  11159  pfxval  11165  pfx00g  11166  pfx0g  11167  fnpfx  11168  pfxlen  11176  swrdccatin1  11216  swrdccat  11226  swrdccat3blem  11230  rexfiuz  11415  qabsor  11501  nn0abscl  11511  nnabscl  11526  climz  11718  climaddc1  11755  climmulc2  11757  climsubc1  11758  climsubc2  11759  climlec2  11767  binomlem  11909  binom  11910  bcxmas  11915  arisum2  11925  explecnv  11931  ef0lem  12086  dvdsval2  12216  dvdsdc  12224  moddvds  12225  dvds0  12232  0dvds  12237  zdvdsdc  12238  dvdscmulr  12246  dvdsmulcr  12247  fsumdvds  12268  dvdslelemd  12269  dvdsabseq  12273  divconjdvds  12275  alzdvds  12280  fzo0dvdseq  12283  odd2np1lem  12298  bitsfzo  12381  bitsmod  12382  0bits  12385  m1bits  12386  bitsinv1lem  12387  bitsinv1  12388  gcdmndc  12391  gcdsupex  12393  gcdsupcl  12394  gcd0val  12396  gcddvds  12399  gcd0id  12415  gcdid0  12416  gcdid  12422  bezoutlema  12435  bezoutlemb  12436  bezoutlembi  12441  dfgcd3  12446  dfgcd2  12450  gcdmultiplez  12457  dvdssq  12467  algcvgblem  12486  lcmmndc  12499  lcm0val  12502  dvdslcm  12506  lcmeq0  12508  lcmgcd  12515  lcmdvds  12516  lcmid  12517  3lcm2e6woprm  12523  6lcm4e12  12524  cncongr2  12541  sqrt2irrap  12617  dfphi2  12657  phiprmpw  12659  crth  12661  phimullem  12662  eulerthlemfi  12665  hashgcdeq  12677  phisum  12678  pceu  12733  pcdiv  12740  pc0  12742  pcqdiv  12745  pcexp  12747  pcxnn0cl  12748  pcxcl  12749  pcxqcl  12750  pcdvdstr  12765  dvdsprmpweqnn  12774  pcaddlem  12777  pcadd  12778  pcfaclem  12787  qexpz  12790  zgz  12811  igz  12812  4sqlem19  12847  ennnfonelemjn  12888  ennnfonelem1  12893  mulg0  13576  subgmulg  13639  zring0  14477  zndvds0  14527  znf1o  14528  znfi  14532  znhash  14533  psr1clfi  14565  plycolemc  15345  rpcxp0  15485  0sgm  15572  1sgmprm  15581  lgslem2  15593  lgsfcl2  15598  lgs0  15605  lgsneg  15616  lgsdilem  15619  lgsdir2lem3  15622  lgsdir  15627  lgsdilem2  15628  lgsdi  15629  lgsne0  15630  lgsprme0  15634  lgsdirnn0  15639  lgsdinn0  15640  apdifflemr  16188  apdiff  16189  iswomni0  16192  nconstwlpolem  16206