Theorem 0z 9457

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 8146	. 2 |- 0 e. RR
2		eqid 2229	. . 3 |- 0 = 0
3	2	3mix1i 1193	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9448	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 948	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 1001   = wceq 1395   e. wcel 2200   RRcr 7998   0cc0 7999   -ucneg 8318   NNcn 9110   ZZcz 9446

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8093  ax-addrcl 8096  ax-rnegex 8108

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6004  df-neg 8320  df-z 9447

This theorem is referenced by:  0zd  9458  nn0ssz  9464  znegcl  9477  nnnle0  9495  zgt0ge1  9505  nn0n0n1ge2b  9526  nn0lt10b  9527  nnm1ge0  9533  gtndiv  9542  msqznn  9547  zeo  9552  nn0ind  9561  fnn0ind  9563  nn0uz  9757  1eluzge0  9769  elnn0dc  9806  eqreznegel  9809  qreccl  9837  qdivcl  9838  irrmul  9842  irrmulap  9843  fz10  10242  fz01en  10249  fzpreddisj  10267  fzshftral  10304  fznn0  10309  fz1ssfz0  10313  fz0sn  10317  fz0tp  10318  fz0to3un2pr  10319  fz0to4untppr  10320  elfz0ubfz0  10321  1fv  10335  fzo0n  10364  lbfzo0  10381  elfzonlteqm1  10416  fzo01  10422  fzo0to2pr  10424  fzo0to3tp  10425  flqge0nn0  10513  divfl0  10516  btwnzge0  10520  modqmulnn  10564  zmodfz  10568  modqid  10571  zmodid2  10574  q0mod  10577  modqmuladdnn0  10590  frecfzennn  10648  xnn0nnen  10659  qexpclz  10782  qsqeqor  10872  facdiv  10960  bcval  10971  bcnn  10979  bcm1k  10982  bcval5  10985  bcpasc  10988  4bc2eq6  10996  hashinfom  11000  iswrd  11073  iswrdiz  11078  wrdexg  11082  wrdfin  11090  wrdnval  11102  wrdred1hash  11115  lsw0  11119  ccatsymb  11137  s111  11164  ccat1st1st  11172  fzowrddc  11179  swrdlen  11184  swrdnd  11191  swrdwrdsymbg  11196  swrds1  11200  pfxval  11206  pfx00g  11207  pfx0g  11208  fnpfx  11209  pfxlen  11217  swrdccatin1  11257  swrdccat  11267  swrdccat3blem  11271  rexfiuz  11500  qabsor  11586  nn0abscl  11596  nnabscl  11611  climz  11803  climaddc1  11840  climmulc2  11842  climsubc1  11843  climsubc2  11844  climlec2  11852  binomlem  11994  binom  11995  bcxmas  12000  arisum2  12010  explecnv  12016  ef0lem  12171  dvdsval2  12301  dvdsdc  12309  moddvds  12310  dvds0  12317  0dvds  12322  zdvdsdc  12323  dvdscmulr  12331  dvdsmulcr  12332  fsumdvds  12353  dvdslelemd  12354  dvdsabseq  12358  divconjdvds  12360  alzdvds  12365  fzo0dvdseq  12368  odd2np1lem  12383  bitsfzo  12466  bitsmod  12467  0bits  12470  m1bits  12471  bitsinv1lem  12472  bitsinv1  12473  gcdmndc  12476  gcdsupex  12478  gcdsupcl  12479  gcd0val  12481  gcddvds  12484  gcd0id  12500  gcdid0  12501  gcdid  12507  bezoutlema  12520  bezoutlemb  12521  bezoutlembi  12526  dfgcd3  12531  dfgcd2  12535  gcdmultiplez  12542  dvdssq  12552  algcvgblem  12571  lcmmndc  12584  lcm0val  12587  dvdslcm  12591  lcmeq0  12593  lcmgcd  12600  lcmdvds  12601  lcmid  12602  3lcm2e6woprm  12608  6lcm4e12  12609  cncongr2  12626  sqrt2irrap  12702  dfphi2  12742  phiprmpw  12744  crth  12746  phimullem  12747  eulerthlemfi  12750  hashgcdeq  12762  phisum  12763  pceu  12818  pcdiv  12825  pc0  12827  pcqdiv  12830  pcexp  12832  pcxnn0cl  12833  pcxcl  12834  pcxqcl  12835  pcdvdstr  12850  dvdsprmpweqnn  12859  pcaddlem  12862  pcadd  12863  pcfaclem  12872  qexpz  12875  zgz  12896  igz  12897  4sqlem19  12932  ennnfonelemjn  12973  ennnfonelem1  12978  mulg0  13662  subgmulg  13725  zring0  14564  zndvds0  14614  znf1o  14615  znfi  14619  znhash  14620  psr1clfi  14652  plycolemc  15432  rpcxp0  15572  0sgm  15659  1sgmprm  15668  lgslem2  15680  lgsfcl2  15685  lgs0  15692  lgsneg  15703  lgsdilem  15706  lgsdir2lem3  15709  lgsdir  15714  lgsdilem2  15715  lgsdi  15716  lgsne0  15717  lgsprme0  15721  lgsdirnn0  15726  lgsdinn0  15727  wlkv0  16080  wlklenvclwlk  16084  apdifflemr  16415  apdiff  16416  iswomni0  16419  nconstwlpolem  16433