Theorem 0z 9483

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 8172	. 2 ⊢ 0 ∈ ℝ
2		eqid 2229	. . 3 ⊢ 0 = 0
3	2	3mix1i 1193	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 9474	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 948	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1001   = wceq 1395   ∈ wcel 2200  ℝcr 8024  0cc0 8025  -cneg 8344  ℕcn 9136  ℤcz 9472

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8119  ax-addrcl 8122  ax-rnegex 8134

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016  df-neg 8346  df-z 9473

This theorem is referenced by:  0zd  9484  nn0ssz  9490  znegcl  9503  nnnle0  9521  zgt0ge1  9531  nn0n0n1ge2b  9552  nn0lt10b  9553  nnm1ge0  9559  gtndiv  9568  msqznn  9573  zeo  9578  nn0ind  9587  fnn0ind  9589  nn0uz  9784  1eluzge0  9801  elnn0dc  9838  eqreznegel  9841  qreccl  9869  qdivcl  9870  irrmul  9874  irrmulap  9875  fz10  10274  fz01en  10281  fzpreddisj  10299  fzshftral  10336  fznn0  10341  fz1ssfz0  10345  fz0sn  10349  fz0tp  10350  fz0to3un2pr  10351  fz0to4untppr  10352  elfz0ubfz0  10353  1fv  10367  fzo0n  10396  lbfzo0  10413  elfzonlteqm1  10448  fzo01  10454  fzo0to2pr  10456  fzo0to3tp  10457  flqge0nn0  10546  divfl0  10549  btwnzge0  10553  modqmulnn  10597  zmodfz  10601  modqid  10604  zmodid2  10607  q0mod  10610  modqmuladdnn0  10623  frecfzennn  10681  xnn0nnen  10692  qexpclz  10815  qsqeqor  10905  facdiv  10993  bcval  11004  bcnn  11012  bcm1k  11015  bcval5  11018  bcpasc  11021  4bc2eq6  11029  hashinfom  11033  iswrd  11108  iswrdiz  11113  wrdexg  11117  wrdfin  11125  wrdnval  11137  wrdred1hash  11150  lsw0  11154  ccatsymb  11172  ccatalpha  11183  s111  11201  ccat1st1st  11211  fzowrddc  11221  swrdlen  11226  swrdnd  11233  swrdwrdsymbg  11238  swrds1  11242  pfxval  11248  pfx00g  11249  pfx0g  11250  fnpfx  11251  pfxlen  11259  swrdccatin1  11299  swrdccat  11309  swrdccat3blem  11313  rexfiuz  11543  qabsor  11629  nn0abscl  11639  nnabscl  11654  climz  11846  climaddc1  11883  climmulc2  11885  climsubc1  11886  climsubc2  11887  climlec2  11895  binomlem  12037  binom  12038  bcxmas  12043  arisum2  12053  explecnv  12059  ef0lem  12214  dvdsval2  12344  dvdsdc  12352  moddvds  12353  dvds0  12360  0dvds  12365  zdvdsdc  12366  dvdscmulr  12374  dvdsmulcr  12375  fsumdvds  12396  dvdslelemd  12397  dvdsabseq  12401  divconjdvds  12403  alzdvds  12408  fzo0dvdseq  12411  odd2np1lem  12426  bitsfzo  12509  bitsmod  12510  0bits  12513  m1bits  12514  bitsinv1lem  12515  bitsinv1  12516  gcdmndc  12519  gcdsupex  12521  gcdsupcl  12522  gcd0val  12524  gcddvds  12527  gcd0id  12543  gcdid0  12544  gcdid  12550  bezoutlema  12563  bezoutlemb  12564  bezoutlembi  12569  dfgcd3  12574  dfgcd2  12578  gcdmultiplez  12585  dvdssq  12595  algcvgblem  12614  lcmmndc  12627  lcm0val  12630  dvdslcm  12634  lcmeq0  12636  lcmgcd  12643  lcmdvds  12644  lcmid  12645  3lcm2e6woprm  12651  6lcm4e12  12652  cncongr2  12669  sqrt2irrap  12745  dfphi2  12785  phiprmpw  12787  crth  12789  phimullem  12790  eulerthlemfi  12793  hashgcdeq  12805  phisum  12806  pceu  12861  pcdiv  12868  pc0  12870  pcqdiv  12873  pcexp  12875  pcxnn0cl  12876  pcxcl  12877  pcxqcl  12878  pcdvdstr  12893  dvdsprmpweqnn  12902  pcaddlem  12905  pcadd  12906  pcfaclem  12915  qexpz  12918  zgz  12939  igz  12940  4sqlem19  12975  ennnfonelemjn  13016  ennnfonelem1  13021  mulg0  13705  subgmulg  13768  zring0  14607  zndvds0  14657  znf1o  14658  znfi  14662  znhash  14663  psr1clfi  14695  plycolemc  15475  rpcxp0  15615  0sgm  15702  1sgmprm  15711  lgslem2  15723  lgsfcl2  15728  lgs0  15735  lgsneg  15746  lgsdilem  15749  lgsdir2lem3  15752  lgsdir  15757  lgsdilem2  15758  lgsdi  15759  lgsne0  15760  lgsprme0  15764  lgsdirnn0  15769  lgsdinn0  15770  usgrexmpldifpr  16093  vdegp1bid  16126  wlkv0  16180  wlklenvclwlk  16184  upgr2wlkdc  16186  clwwlkccatlem  16209  eupthfi  16260  apdifflemr  16601  apdiff  16602  iswomni0  16605  nconstwlpolem  16619