Theorem 0z 9584

Description: Zero is an integer. (Contributed by NM, 12-Jan-2002.)

Assertion

Ref	Expression
0z	⊢ 0 ∈ ℤ

Proof of Theorem 0z

Step	Hyp	Ref	Expression
1		0re 8270	. 2 ⊢ 0 ∈ ℝ
2		eqid 2232	. . 3 ⊢ 0 = 0
3	2	3mix1i 1196	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 9575	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 951	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1004   = wceq 1398   ∈ wcel 2203  ℝcr 8122  0cc0 8123  -cneg 8441  ℕcn 9233  ℤcz 9573

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 2214  ax-1re 8217  ax-addrcl 8220  ax-rnegex 8232

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-rab 2529  df-v 2814  df-un 3214  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-br 4109  df-iota 5311  df-fv 5359  df-ov 6052  df-neg 8443  df-z 9574

This theorem is referenced by:  0zd  9585  nn0ssz  9591  znegcl  9604  nnnle0  9622  zgt0ge1  9632  nn0n0n1ge2b  9653  nn0lt10b  9654  nnm1ge0  9660  gtndiv  9669  msqznn  9674  zeo  9679  nn0ind  9688  fnn0ind  9690  nn0uz  9885  1eluzge0  9902  elnn0dc  9939  eqreznegel  9942  qreccl  9970  qdivcl  9971  irrmul  9975  irrmulap  9976  fz10  10376  fz01en  10383  fzpreddisj  10401  fzshftral  10438  fznn0  10443  fz1ssfz0  10447  fz0sn  10451  fz0tp  10452  fz0to3un2pr  10453  fz0to4untppr  10454  elfz0ubfz0  10455  1fv  10469  fzo0n  10498  lbfzo0  10515  elfzonlteqm1  10551  fzo01  10557  fzo0to2pr  10559  fzo0to3tp  10560  flqge0nn0  10649  divfl0  10652  btwnzge0  10656  modqmulnn  10700  zmodfz  10704  modqid  10707  zmodid2  10710  q0mod  10713  modqmuladdnn0  10726  frecfzennn  10784  xnn0nnen  10795  qexpclz  10918  qsqeqor  11008  facdiv  11096  bcval  11107  bcnn  11115  bcm1k  11118  bcval5  11121  bcpasc  11124  4bc2eq6  11132  hashinfom  11136  hashfibc  11200  iswrd  11219  iswrdiz  11224  wrdexg  11228  wrdfin  11236  wrdnval  11248  wrdred1hash  11261  lsw0  11265  ccatsymb  11283  ccatalpha  11294  s111  11312  ccat1st1st  11322  fzowrddc  11332  swrdlen  11337  swrdnd  11344  swrdwrdsymbg  11349  swrds1  11353  pfxval  11359  pfx00g  11360  pfx0g  11361  fnpfx  11362  pfxlen  11370  swrdccatin1  11410  swrdccat  11420  swrdccat3blem  11424  rexfiuz  11667  qabsor  11753  nn0abscl  11763  nnabscl  11778  climz  11970  climaddc1  12007  climmulc2  12009  climsubc1  12010  climsubc2  12011  climlec2  12019  binomlem  12162  binom  12163  bcxmas  12168  arisum2  12178  explecnv  12184  ef0lem  12339  dvdsval2  12469  dvdsdc  12477  moddvds  12478  dvds0  12485  0dvds  12490  zdvdsdc  12491  dvdscmulr  12499  dvdsmulcr  12500  fsumdvds  12521  dvdslelemd  12522  dvdsabseq  12526  divconjdvds  12528  alzdvds  12533  fzo0dvdseq  12536  odd2np1lem  12551  bitsfzo  12634  bitsmod  12635  0bits  12638  m1bits  12639  bitsinv1lem  12640  bitsinv1  12641  gcdmndc  12644  gcdsupex  12646  gcdsupcl  12647  gcd0val  12649  gcddvds  12652  gcd0id  12668  gcdid0  12669  gcdid  12675  bezoutlema  12688  bezoutlemb  12689  bezoutlembi  12694  dfgcd3  12699  dfgcd2  12703  gcdmultiplez  12710  dvdssq  12720  algcvgblem  12739  lcmmndc  12752  lcm0val  12755  dvdslcm  12759  lcmeq0  12761  lcmgcd  12768  lcmdvds  12769  lcmid  12770  3lcm2e6woprm  12776  6lcm4e12  12777  cncongr2  12794  sqrt2irrap  12870  dfphi2  12910  phiprmpw  12912  crth  12914  phimullem  12915  eulerthlemfi  12918  hashgcdeq  12930  phisum  12931  pceu  12986  pcdiv  12993  pc0  12995  pcqdiv  12998  pcexp  13000  pcxnn0cl  13001  pcxcl  13002  pcxqcl  13003  pcdvdstr  13018  dvdsprmpweqnn  13027  pcaddlem  13030  pcadd  13031  pcfaclem  13040  qexpz  13043  zgz  13064  igz  13065  4sqlem19  13100  ennnfonelemjn  13142  ennnfonelem1  13147  mulg0  13831  subgmulg  13894  zring0  14735  zndvds0  14785  znf1o  14786  znfi  14790  znhash  14791  psr1clfi  14830  plycolemc  15610  rpcxp0  15750  0sgm  15840  1sgmprm  15849  lgslem2  15861  lgsfcl2  15866  lgs0  15873  lgsneg  15884  lgsdilem  15887  lgsdir2lem3  15890  lgsdir  15895  lgsdilem2  15896  lgsdi  15897  lgsne0  15898  lgsprme0  15902  lgsdirnn0  15907  lgsdinn0  15908  usgrexmpldifpr  16231  vdegp1bid  16297  wlkv0  16351  wlklenvclwlk  16355  upgr2wlkdc  16359  clwwlkccatlem  16382  eupthfi  16433  trlsegvdeglem6  16447  konigsbergvtx  16464  konigsbergiedg  16465  konigsbergumgr  16469  konigsberglem1  16470  konigsberglem2  16471  konigsberglem3  16472  konigsberglem5  16474  konigsberg  16475  apdifflemr  16818  apdiff  16819  qdiff  16820  iswomni0  16823  nconstwlpolem  16837