Theorem 0z 9331

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 8021	. 2 |- 0 e. RR
2		eqid 2193	. . 3 |- 0 = 0
3	2	3mix1i 1171	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9322	. 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 1364   e. wcel 2164   RRcr 7873   0cc0 7874   -ucneg 8193   NNcn 8984   ZZcz 9320

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-1re 7968  ax-addrcl 7971  ax-rnegex 7983

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-rab 2481  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263  df-ov 5922  df-neg 8195  df-z 9321

This theorem is referenced by:  0zd  9332  nn0ssz  9338  znegcl  9351  zgt0ge1  9378  nn0n0n1ge2b  9399  nn0lt10b  9400  nnm1ge0  9406  gtndiv  9415  msqznn  9420  zeo  9425  nn0ind  9434  fnn0ind  9436  nn0uz  9630  1eluzge0  9642  elnn0dc  9679  eqreznegel  9682  qreccl  9710  qdivcl  9711  irrmul  9715  irrmulap  9716  fz10  10115  fz01en  10122  fzpreddisj  10140  fzshftral  10177  fznn0  10182  fz1ssfz0  10186  fz0sn  10190  fz0tp  10191  fz0to3un2pr  10192  fz0to4untppr  10193  elfz0ubfz0  10194  1fv  10208  lbfzo0  10251  elfzonlteqm1  10280  fzo01  10286  fzo0to2pr  10288  fzo0to3tp  10289  flqge0nn0  10365  divfl0  10368  btwnzge0  10372  modqmulnn  10416  zmodfz  10420  modqid  10423  zmodid2  10426  q0mod  10429  modqmuladdnn0  10442  frecfzennn  10500  xnn0nnen  10511  qexpclz  10634  qsqeqor  10724  facdiv  10812  bcval  10823  bcnn  10831  bcm1k  10834  bcval5  10837  bcpasc  10840  4bc2eq6  10848  hashinfom  10852  iswrd  10919  iswrdiz  10924  wrdexg  10928  wrdfin  10936  wrdnval  10947  wrdred1hash  10960  rexfiuz  11136  qabsor  11222  nn0abscl  11232  nnabscl  11247  climz  11438  climaddc1  11475  climmulc2  11477  climsubc1  11478  climsubc2  11479  climlec2  11487  binomlem  11629  binom  11630  bcxmas  11635  arisum2  11645  explecnv  11651  ef0lem  11806  dvdsval2  11936  dvdsdc  11944  moddvds  11945  dvds0  11952  0dvds  11957  zdvdsdc  11958  dvdscmulr  11966  dvdsmulcr  11967  dvdslelemd  11988  dvdsabseq  11992  divconjdvds  11994  alzdvds  11999  fzo0dvdseq  12002  odd2np1lem  12016  gcdmndc  12084  gcdsupex  12097  gcdsupcl  12098  gcd0val  12100  gcddvds  12103  gcd0id  12119  gcdid0  12120  gcdid  12126  bezoutlema  12139  bezoutlemb  12140  bezoutlembi  12145  dfgcd3  12150  dfgcd2  12154  gcdmultiplez  12161  dvdssq  12171  algcvgblem  12190  lcmmndc  12203  lcm0val  12206  dvdslcm  12210  lcmeq0  12212  lcmgcd  12219  lcmdvds  12220  lcmid  12221  3lcm2e6woprm  12227  6lcm4e12  12228  cncongr2  12245  sqrt2irrap  12321  dfphi2  12361  phiprmpw  12363  crth  12365  phimullem  12366  eulerthlemfi  12369  hashgcdeq  12380  phisum  12381  pceu  12436  pcdiv  12443  pc0  12445  pcqdiv  12448  pcexp  12450  pcxnn0cl  12451  pcxcl  12452  pcxqcl  12453  pcdvdstr  12468  dvdsprmpweqnn  12477  pcaddlem  12480  pcadd  12481  pcfaclem  12490  qexpz  12493  zgz  12514  igz  12515  4sqlem19  12550  ennnfonelemjn  12562  ennnfonelem1  12567  mulg0  13198  subgmulg  13261  zring0  14099  zndvds0  14149  znf1o  14150  znfi  14154  znhash  14155  plycolemc  14936  rpcxp0  15074  lgslem2  15158  lgsfcl2  15163  lgs0  15170  lgsneg  15181  lgsdilem  15184  lgsdir2lem3  15187  lgsdir  15192  lgsdilem2  15193  lgsdi  15194  lgsne0  15195  lgsprme0  15199  lgsdirnn0  15204  lgsdinn0  15205  apdifflemr  15607  apdiff  15608  iswomni0  15611  nconstwlpolem  15625