Theorem 0z 9593

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 8279	. 2 ⊢ 0 ∈ ℝ
2		eqid 2234	. . 3 ⊢ 0 = 0
3	2	3mix1i 1196	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 9584	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 951	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1004   = wceq 1398   ∈ wcel 2205  ℝcr 8131  0cc0 8132  -cneg 8450  ℕcn 9242  ℤcz 9582

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 2216  ax-1re 8226  ax-addrcl 8229  ax-rnegex 8241

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 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-rab 2531  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-iota 5314  df-fv 5362  df-ov 6055  df-neg 8452  df-z 9583

This theorem is referenced by:  0zd  9594  nn0ssz  9600  znegcl  9613  nnnle0  9631  zgt0ge1  9641  nn0n0n1ge2b  9663  nn0lt10b  9664  nnm1ge0  9670  gtndiv  9679  msqznn  9684  zeo  9689  nn0ind  9698  fnn0ind  9700  nn0uz  9895  1eluzge0  9912  elnn0dc  9949  eqreznegel  9952  qreccl  9980  qdivcl  9981  irrmul  9985  irrmulap  9986  fz10  10386  fz01en  10393  fzpreddisj  10412  fzshftral  10449  fznn0  10454  fz1ssfz0  10458  fz0sn  10462  fz0tp  10463  fz0to3un2pr  10464  fz0to4untppr  10465  elfz0ubfz0  10466  1fv  10480  fzo0n  10509  lbfzo0  10526  elfzonlteqm1  10562  fzo01  10568  fzo0to2pr  10570  fzo0to3tp  10571  flqge0nn0  10660  divfl0  10663  btwnzge0  10667  modqmulnn  10711  zmodfz  10715  modqid  10718  zmodid2  10721  q0mod  10724  modqmuladdnn0  10737  frecfzennn  10795  xnn0nnen  10806  qexpclz  10929  qsqeqor  11019  facdiv  11108  bcval  11119  bcnn  11127  bcm1k  11130  bcval5  11133  bcpasc  11136  4bc2eq6  11145  hashinfom  11149  hashfibc  11215  iswrd  11234  iswrdiz  11239  wrdexg  11243  wrdfin  11251  wrdnval  11263  wrdred1hash  11276  lsw0  11280  ccatsymb  11298  ccatalpha  11309  s111  11327  ccat1st1st  11337  fzowrddc  11347  swrdlen  11352  swrdnd  11359  swrdwrdsymbg  11364  swrds1  11368  pfxval  11374  pfx00g  11375  pfx0g  11376  fnpfx  11377  pfxlen  11385  swrdccatin1  11425  swrdccat  11435  swrdccat3blem  11439  rexfiuz  11682  qabsor  11768  nn0abscl  11778  nnabscl  11793  climz  11985  climaddc1  12022  climmulc2  12024  climsubc1  12025  climsubc2  12026  climlec2  12034  binomlem  12177  binom  12178  bcxmas  12183  arisum2  12193  explecnv  12199  ef0lem  12354  dvdsval2  12484  dvdsdc  12492  moddvds  12493  dvds0  12500  0dvds  12505  zdvdsdc  12506  dvdscmulr  12514  dvdsmulcr  12515  fsumdvds  12536  dvdslelemd  12537  dvdsabseq  12541  divconjdvds  12543  alzdvds  12548  fzo0dvdseq  12551  odd2np1lem  12566  bitsfzo  12649  bitsmod  12650  0bits  12653  m1bits  12654  bitsinv1lem  12655  bitsinv1  12656  gcdmndc  12659  gcdsupex  12661  gcdsupcl  12662  gcd0val  12664  gcddvds  12667  gcd0id  12683  gcdid0  12684  gcdid  12690  bezoutlema  12703  bezoutlemb  12704  bezoutlembi  12709  dfgcd3  12714  dfgcd2  12718  gcdmultiplez  12725  dvdssq  12735  algcvgblem  12754  lcmmndc  12767  lcm0val  12770  dvdslcm  12774  lcmeq0  12776  lcmgcd  12783  lcmdvds  12784  lcmid  12785  3lcm2e6woprm  12791  6lcm4e12  12792  cncongr2  12809  sqrt2irrap  12885  dfphi2  12925  phiprmpw  12927  crth  12929  phimullem  12930  eulerthlemfi  12933  hashgcdeq  12945  phisum  12946  pceu  13001  pcdiv  13008  pc0  13010  pcqdiv  13013  pcexp  13015  pcxnn0cl  13016  pcxcl  13017  pcxqcl  13018  pcdvdstr  13033  dvdsprmpweqnn  13042  pcaddlem  13045  pcadd  13046  pcfaclem  13055  qexpz  13058  zgz  13079  igz  13080  4sqlem19  13115  ballotfilemonn  13148  ballotfilem2  13153  ballotfilemfc0  13157  ballotfilemfcc  13158  ballotfilemodife  13162  ennnfonelemjn  13174  ennnfonelem1  13179  mulg0  13863  subgmulg  13926  zring0  14797  zndvds0  14847  znf1o  14848  znfi  14852  znhash  14853  psr1clfi  14892  plycolemc  15672  rpcxp0  15812  0sgm  15902  1sgmprm  15911  lgslem2  15923  lgsfcl2  15928  lgs0  15935  lgsneg  15946  lgsdilem  15949  lgsdir2lem3  15952  lgsdir  15957  lgsdilem2  15958  lgsdi  15959  lgsne0  15960  lgsprme0  15964  lgsdirnn0  15969  lgsdinn0  15970  usgrexmpldifpr  16293  vdegp1bid  16359  wlkv0  16413  wlklenvclwlk  16417  upgr2wlkdc  16421  clwwlkccatlem  16444  eupthfi  16495  trlsegvdeglem6  16509  konigsbergvtx  16526  konigsbergiedg  16527  konigsbergumgr  16531  konigsberglem1  16532  konigsberglem2  16533  konigsberglem3  16534  konigsberglem5  16536  konigsberg  16537  apdifflemr  16880  apdiff  16881  qdiff  16882  iswomni0  16885  nconstwlpolem  16900