Theorem 0z 9534

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 8222	. 2 |- 0 e. RR
2		eqid 2231	. . 3 |- 0 = 0
3	2	3mix1i 1196	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9525	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 951	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 1004   = wceq 1398   e. wcel 2202   RRcr 8074   0cc0 8075   -ucneg 8393   NNcn 9185   ZZcz 9523

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-1re 8169  ax-addrcl 8172  ax-rnegex 8184

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-rab 2520  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031  df-neg 8395  df-z 9524

This theorem is referenced by:  0zd  9535  nn0ssz  9541  znegcl  9554  nnnle0  9572  zgt0ge1  9582  nn0n0n1ge2b  9603  nn0lt10b  9604  nnm1ge0  9610  gtndiv  9619  msqznn  9624  zeo  9629  nn0ind  9638  fnn0ind  9640  nn0uz  9835  1eluzge0  9852  elnn0dc  9889  eqreznegel  9892  qreccl  9920  qdivcl  9921  irrmul  9925  irrmulap  9926  fz10  10326  fz01en  10333  fzpreddisj  10351  fzshftral  10388  fznn0  10393  fz1ssfz0  10397  fz0sn  10401  fz0tp  10402  fz0to3un2pr  10403  fz0to4untppr  10404  elfz0ubfz0  10405  1fv  10419  fzo0n  10448  lbfzo0  10465  elfzonlteqm1  10501  fzo01  10507  fzo0to2pr  10509  fzo0to3tp  10510  flqge0nn0  10599  divfl0  10602  btwnzge0  10606  modqmulnn  10650  zmodfz  10654  modqid  10657  zmodid2  10660  q0mod  10663  modqmuladdnn0  10676  frecfzennn  10734  xnn0nnen  10745  qexpclz  10868  qsqeqor  10958  facdiv  11046  bcval  11057  bcnn  11065  bcm1k  11068  bcval5  11071  bcpasc  11074  4bc2eq6  11082  hashinfom  11086  iswrd  11164  iswrdiz  11169  wrdexg  11173  wrdfin  11181  wrdnval  11193  wrdred1hash  11206  lsw0  11210  ccatsymb  11228  ccatalpha  11239  s111  11257  ccat1st1st  11267  fzowrddc  11277  swrdlen  11282  swrdnd  11289  swrdwrdsymbg  11294  swrds1  11298  pfxval  11304  pfx00g  11305  pfx0g  11306  fnpfx  11307  pfxlen  11315  swrdccatin1  11355  swrdccat  11365  swrdccat3blem  11369  rexfiuz  11612  qabsor  11698  nn0abscl  11708  nnabscl  11723  climz  11915  climaddc1  11952  climmulc2  11954  climsubc1  11955  climsubc2  11956  climlec2  11964  binomlem  12107  binom  12108  bcxmas  12113  arisum2  12123  explecnv  12129  ef0lem  12284  dvdsval2  12414  dvdsdc  12422  moddvds  12423  dvds0  12430  0dvds  12435  zdvdsdc  12436  dvdscmulr  12444  dvdsmulcr  12445  fsumdvds  12466  dvdslelemd  12467  dvdsabseq  12471  divconjdvds  12473  alzdvds  12478  fzo0dvdseq  12481  odd2np1lem  12496  bitsfzo  12579  bitsmod  12580  0bits  12583  m1bits  12584  bitsinv1lem  12585  bitsinv1  12586  gcdmndc  12589  gcdsupex  12591  gcdsupcl  12592  gcd0val  12594  gcddvds  12597  gcd0id  12613  gcdid0  12614  gcdid  12620  bezoutlema  12633  bezoutlemb  12634  bezoutlembi  12639  dfgcd3  12644  dfgcd2  12648  gcdmultiplez  12655  dvdssq  12665  algcvgblem  12684  lcmmndc  12697  lcm0val  12700  dvdslcm  12704  lcmeq0  12706  lcmgcd  12713  lcmdvds  12714  lcmid  12715  3lcm2e6woprm  12721  6lcm4e12  12722  cncongr2  12739  sqrt2irrap  12815  dfphi2  12855  phiprmpw  12857  crth  12859  phimullem  12860  eulerthlemfi  12863  hashgcdeq  12875  phisum  12876  pceu  12931  pcdiv  12938  pc0  12940  pcqdiv  12943  pcexp  12945  pcxnn0cl  12946  pcxcl  12947  pcxqcl  12948  pcdvdstr  12963  dvdsprmpweqnn  12972  pcaddlem  12975  pcadd  12976  pcfaclem  12985  qexpz  12988  zgz  13009  igz  13010  4sqlem19  13045  ennnfonelemjn  13086  ennnfonelem1  13091  mulg0  13775  subgmulg  13838  zring0  14679  zndvds0  14729  znf1o  14730  znfi  14734  znhash  14735  psr1clfi  14772  plycolemc  15552  rpcxp0  15692  0sgm  15782  1sgmprm  15791  lgslem2  15803  lgsfcl2  15808  lgs0  15815  lgsneg  15826  lgsdilem  15829  lgsdir2lem3  15832  lgsdir  15837  lgsdilem2  15838  lgsdi  15839  lgsne0  15840  lgsprme0  15844  lgsdirnn0  15849  lgsdinn0  15850  usgrexmpldifpr  16173  vdegp1bid  16239  wlkv0  16293  wlklenvclwlk  16297  upgr2wlkdc  16301  clwwlkccatlem  16324  eupthfi  16375  trlsegvdeglem6  16389  konigsbergvtx  16406  konigsbergiedg  16407  konigsbergumgr  16411  konigsberglem1  16412  konigsberglem2  16413  konigsberglem3  16414  konigsberglem5  16416  konigsberg  16417  apdifflemr  16762  apdiff  16763  qdiff  16764  iswomni0  16767  nconstwlpolem  16781