Theorem 0z 9382

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 8071	. 2 |- 0 e. RR
2		eqid 2204	. . 3 |- 0 = 0
3	2	3mix1i 1171	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9373	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 944	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 979   = wceq 1372   e. wcel 2175   RRcr 7923   0cc0 7924   -ucneg 8243   NNcn 9035   ZZcz 9371

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-1re 8018  ax-addrcl 8021  ax-rnegex 8033

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-rab 2492  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-iota 5231  df-fv 5278  df-ov 5946  df-neg 8245  df-z 9372

This theorem is referenced by:  0zd  9383  nn0ssz  9389  znegcl  9402  nnnle0  9420  zgt0ge1  9430  nn0n0n1ge2b  9451  nn0lt10b  9452  nnm1ge0  9458  gtndiv  9467  msqznn  9472  zeo  9477  nn0ind  9486  fnn0ind  9488  nn0uz  9682  1eluzge0  9694  elnn0dc  9731  eqreznegel  9734  qreccl  9762  qdivcl  9763  irrmul  9767  irrmulap  9768  fz10  10167  fz01en  10174  fzpreddisj  10192  fzshftral  10229  fznn0  10234  fz1ssfz0  10238  fz0sn  10242  fz0tp  10243  fz0to3un2pr  10244  fz0to4untppr  10245  elfz0ubfz0  10246  1fv  10260  lbfzo0  10303  elfzonlteqm1  10337  fzo01  10343  fzo0to2pr  10345  fzo0to3tp  10346  flqge0nn0  10434  divfl0  10437  btwnzge0  10441  modqmulnn  10485  zmodfz  10489  modqid  10492  zmodid2  10495  q0mod  10498  modqmuladdnn0  10511  frecfzennn  10569  xnn0nnen  10580  qexpclz  10703  qsqeqor  10793  facdiv  10881  bcval  10892  bcnn  10900  bcm1k  10903  bcval5  10906  bcpasc  10909  4bc2eq6  10917  hashinfom  10921  iswrd  10994  iswrdiz  10999  wrdexg  11003  wrdfin  11011  wrdnval  11022  wrdred1hash  11035  lsw0  11039  ccatsymb  11056  s111  11083  ccat1st1st  11091  rexfiuz  11271  qabsor  11357  nn0abscl  11367  nnabscl  11382  climz  11574  climaddc1  11611  climmulc2  11613  climsubc1  11614  climsubc2  11615  climlec2  11623  binomlem  11765  binom  11766  bcxmas  11771  arisum2  11781  explecnv  11787  ef0lem  11942  dvdsval2  12072  dvdsdc  12080  moddvds  12081  dvds0  12088  0dvds  12093  zdvdsdc  12094  dvdscmulr  12102  dvdsmulcr  12103  fsumdvds  12124  dvdslelemd  12125  dvdsabseq  12129  divconjdvds  12131  alzdvds  12136  fzo0dvdseq  12139  odd2np1lem  12154  bitsfzo  12237  bitsmod  12238  0bits  12241  m1bits  12242  bitsinv1lem  12243  bitsinv1  12244  gcdmndc  12247  gcdsupex  12249  gcdsupcl  12250  gcd0val  12252  gcddvds  12255  gcd0id  12271  gcdid0  12272  gcdid  12278  bezoutlema  12291  bezoutlemb  12292  bezoutlembi  12297  dfgcd3  12302  dfgcd2  12306  gcdmultiplez  12313  dvdssq  12323  algcvgblem  12342  lcmmndc  12355  lcm0val  12358  dvdslcm  12362  lcmeq0  12364  lcmgcd  12371  lcmdvds  12372  lcmid  12373  3lcm2e6woprm  12379  6lcm4e12  12380  cncongr2  12397  sqrt2irrap  12473  dfphi2  12513  phiprmpw  12515  crth  12517  phimullem  12518  eulerthlemfi  12521  hashgcdeq  12533  phisum  12534  pceu  12589  pcdiv  12596  pc0  12598  pcqdiv  12601  pcexp  12603  pcxnn0cl  12604  pcxcl  12605  pcxqcl  12606  pcdvdstr  12621  dvdsprmpweqnn  12630  pcaddlem  12633  pcadd  12634  pcfaclem  12643  qexpz  12646  zgz  12667  igz  12668  4sqlem19  12703  ennnfonelemjn  12744  ennnfonelem1  12749  mulg0  13432  subgmulg  13495  zring0  14333  zndvds0  14383  znf1o  14384  znfi  14388  znhash  14389  psr1clfi  14421  plycolemc  15201  rpcxp0  15341  0sgm  15428  1sgmprm  15437  lgslem2  15449  lgsfcl2  15454  lgs0  15461  lgsneg  15472  lgsdilem  15475  lgsdir2lem3  15478  lgsdir  15483  lgsdilem2  15484  lgsdi  15485  lgsne0  15486  lgsprme0  15490  lgsdirnn0  15495  lgsdinn0  15496  apdifflemr  15948  apdiff  15949  iswomni0  15952  nconstwlpolem  15966