Theorem 0z 9490

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 8179	. 2 ⊢ 0 ∈ ℝ
2		eqid 2231	. . 3 ⊢ 0 = 0
3	2	3mix1i 1195	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 9481	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 950	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1003   = wceq 1397   ∈ wcel 2202  ℝcr 8031  0cc0 8032  -cneg 8351  ℕcn 9143  ℤcz 9479

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1re 8126  ax-addrcl 8129  ax-rnegex 8141

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021  df-neg 8353  df-z 9480

This theorem is referenced by:  0zd  9491  nn0ssz  9497  znegcl  9510  nnnle0  9528  zgt0ge1  9538  nn0n0n1ge2b  9559  nn0lt10b  9560  nnm1ge0  9566  gtndiv  9575  msqznn  9580  zeo  9585  nn0ind  9594  fnn0ind  9596  nn0uz  9791  1eluzge0  9808  elnn0dc  9845  eqreznegel  9848  qreccl  9876  qdivcl  9877  irrmul  9881  irrmulap  9882  fz10  10281  fz01en  10288  fzpreddisj  10306  fzshftral  10343  fznn0  10348  fz1ssfz0  10352  fz0sn  10356  fz0tp  10357  fz0to3un2pr  10358  fz0to4untppr  10359  elfz0ubfz0  10360  1fv  10374  fzo0n  10403  lbfzo0  10420  elfzonlteqm1  10456  fzo01  10462  fzo0to2pr  10464  fzo0to3tp  10465  flqge0nn0  10554  divfl0  10557  btwnzge0  10561  modqmulnn  10605  zmodfz  10609  modqid  10612  zmodid2  10615  q0mod  10618  modqmuladdnn0  10631  frecfzennn  10689  xnn0nnen  10700  qexpclz  10823  qsqeqor  10913  facdiv  11001  bcval  11012  bcnn  11020  bcm1k  11023  bcval5  11026  bcpasc  11029  4bc2eq6  11037  hashinfom  11041  iswrd  11116  iswrdiz  11121  wrdexg  11125  wrdfin  11133  wrdnval  11145  wrdred1hash  11158  lsw0  11162  ccatsymb  11180  ccatalpha  11191  s111  11209  ccat1st1st  11219  fzowrddc  11229  swrdlen  11234  swrdnd  11241  swrdwrdsymbg  11246  swrds1  11250  pfxval  11256  pfx00g  11257  pfx0g  11258  fnpfx  11259  pfxlen  11267  swrdccatin1  11307  swrdccat  11317  swrdccat3blem  11321  rexfiuz  11551  qabsor  11637  nn0abscl  11647  nnabscl  11662  climz  11854  climaddc1  11891  climmulc2  11893  climsubc1  11894  climsubc2  11895  climlec2  11903  binomlem  12046  binom  12047  bcxmas  12052  arisum2  12062  explecnv  12068  ef0lem  12223  dvdsval2  12353  dvdsdc  12361  moddvds  12362  dvds0  12369  0dvds  12374  zdvdsdc  12375  dvdscmulr  12383  dvdsmulcr  12384  fsumdvds  12405  dvdslelemd  12406  dvdsabseq  12410  divconjdvds  12412  alzdvds  12417  fzo0dvdseq  12420  odd2np1lem  12435  bitsfzo  12518  bitsmod  12519  0bits  12522  m1bits  12523  bitsinv1lem  12524  bitsinv1  12525  gcdmndc  12528  gcdsupex  12530  gcdsupcl  12531  gcd0val  12533  gcddvds  12536  gcd0id  12552  gcdid0  12553  gcdid  12559  bezoutlema  12572  bezoutlemb  12573  bezoutlembi  12578  dfgcd3  12583  dfgcd2  12587  gcdmultiplez  12594  dvdssq  12604  algcvgblem  12623  lcmmndc  12636  lcm0val  12639  dvdslcm  12643  lcmeq0  12645  lcmgcd  12652  lcmdvds  12653  lcmid  12654  3lcm2e6woprm  12660  6lcm4e12  12661  cncongr2  12678  sqrt2irrap  12754  dfphi2  12794  phiprmpw  12796  crth  12798  phimullem  12799  eulerthlemfi  12802  hashgcdeq  12814  phisum  12815  pceu  12870  pcdiv  12877  pc0  12879  pcqdiv  12882  pcexp  12884  pcxnn0cl  12885  pcxcl  12886  pcxqcl  12887  pcdvdstr  12902  dvdsprmpweqnn  12911  pcaddlem  12914  pcadd  12915  pcfaclem  12924  qexpz  12927  zgz  12948  igz  12949  4sqlem19  12984  ennnfonelemjn  13025  ennnfonelem1  13030  mulg0  13714  subgmulg  13777  zring0  14617  zndvds0  14667  znf1o  14668  znfi  14672  znhash  14673  psr1clfi  14705  plycolemc  15485  rpcxp0  15625  0sgm  15712  1sgmprm  15721  lgslem2  15733  lgsfcl2  15738  lgs0  15745  lgsneg  15756  lgsdilem  15759  lgsdir2lem3  15762  lgsdir  15767  lgsdilem2  15768  lgsdi  15769  lgsne0  15770  lgsprme0  15774  lgsdirnn0  15779  lgsdinn0  15780  usgrexmpldifpr  16103  vdegp1bid  16169  wlkv0  16223  wlklenvclwlk  16227  upgr2wlkdc  16231  clwwlkccatlem  16254  eupthfi  16305  trlsegvdeglem6  16319  apdifflemr  16672  apdiff  16673  iswomni0  16676  nconstwlpolem  16690