Theorem 0z 9495

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

Syntax hints:   ∨ w3o 1003   = wceq 1397   ∈ wcel 2201  ℝcr 8036  0cc0 8037  -cneg 8356  ℕcn 9148  ℤcz 9484

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 2212  ax-1re 8131  ax-addrcl 8134  ax-rnegex 8146

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-rex 2515  df-rab 2518  df-v 2803  df-un 3203  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-br 4090  df-iota 5288  df-fv 5336  df-ov 6026  df-neg 8358  df-z 9485

This theorem is referenced by:  0zd  9496  nn0ssz  9502  znegcl  9515  nnnle0  9533  zgt0ge1  9543  nn0n0n1ge2b  9564  nn0lt10b  9565  nnm1ge0  9571  gtndiv  9580  msqznn  9585  zeo  9590  nn0ind  9599  fnn0ind  9601  nn0uz  9796  1eluzge0  9813  elnn0dc  9850  eqreznegel  9853  qreccl  9881  qdivcl  9882  irrmul  9886  irrmulap  9887  fz10  10286  fz01en  10293  fzpreddisj  10311  fzshftral  10348  fznn0  10353  fz1ssfz0  10357  fz0sn  10361  fz0tp  10362  fz0to3un2pr  10363  fz0to4untppr  10364  elfz0ubfz0  10365  1fv  10379  fzo0n  10408  lbfzo0  10425  elfzonlteqm1  10461  fzo01  10467  fzo0to2pr  10469  fzo0to3tp  10470  flqge0nn0  10559  divfl0  10562  btwnzge0  10566  modqmulnn  10610  zmodfz  10614  modqid  10617  zmodid2  10620  q0mod  10623  modqmuladdnn0  10636  frecfzennn  10694  xnn0nnen  10705  qexpclz  10828  qsqeqor  10918  facdiv  11006  bcval  11017  bcnn  11025  bcm1k  11028  bcval5  11031  bcpasc  11034  4bc2eq6  11042  hashinfom  11046  iswrd  11124  iswrdiz  11129  wrdexg  11133  wrdfin  11141  wrdnval  11153  wrdred1hash  11166  lsw0  11170  ccatsymb  11188  ccatalpha  11199  s111  11217  ccat1st1st  11227  fzowrddc  11237  swrdlen  11242  swrdnd  11249  swrdwrdsymbg  11254  swrds1  11258  pfxval  11264  pfx00g  11265  pfx0g  11266  fnpfx  11267  pfxlen  11275  swrdccatin1  11315  swrdccat  11325  swrdccat3blem  11329  rexfiuz  11572  qabsor  11658  nn0abscl  11668  nnabscl  11683  climz  11875  climaddc1  11912  climmulc2  11914  climsubc1  11915  climsubc2  11916  climlec2  11924  binomlem  12067  binom  12068  bcxmas  12073  arisum2  12083  explecnv  12089  ef0lem  12244  dvdsval2  12374  dvdsdc  12382  moddvds  12383  dvds0  12390  0dvds  12395  zdvdsdc  12396  dvdscmulr  12404  dvdsmulcr  12405  fsumdvds  12426  dvdslelemd  12427  dvdsabseq  12431  divconjdvds  12433  alzdvds  12438  fzo0dvdseq  12441  odd2np1lem  12456  bitsfzo  12539  bitsmod  12540  0bits  12543  m1bits  12544  bitsinv1lem  12545  bitsinv1  12546  gcdmndc  12549  gcdsupex  12551  gcdsupcl  12552  gcd0val  12554  gcddvds  12557  gcd0id  12573  gcdid0  12574  gcdid  12580  bezoutlema  12593  bezoutlemb  12594  bezoutlembi  12599  dfgcd3  12604  dfgcd2  12608  gcdmultiplez  12615  dvdssq  12625  algcvgblem  12644  lcmmndc  12657  lcm0val  12660  dvdslcm  12664  lcmeq0  12666  lcmgcd  12673  lcmdvds  12674  lcmid  12675  3lcm2e6woprm  12681  6lcm4e12  12682  cncongr2  12699  sqrt2irrap  12775  dfphi2  12815  phiprmpw  12817  crth  12819  phimullem  12820  eulerthlemfi  12823  hashgcdeq  12835  phisum  12836  pceu  12891  pcdiv  12898  pc0  12900  pcqdiv  12903  pcexp  12905  pcxnn0cl  12906  pcxcl  12907  pcxqcl  12908  pcdvdstr  12923  dvdsprmpweqnn  12932  pcaddlem  12935  pcadd  12936  pcfaclem  12945  qexpz  12948  zgz  12969  igz  12970  4sqlem19  13005  ennnfonelemjn  13046  ennnfonelem1  13051  mulg0  13735  subgmulg  13798  zring0  14638  zndvds0  14688  znf1o  14689  znfi  14693  znhash  14694  psr1clfi  14731  plycolemc  15511  rpcxp0  15651  0sgm  15738  1sgmprm  15747  lgslem2  15759  lgsfcl2  15764  lgs0  15771  lgsneg  15782  lgsdilem  15785  lgsdir2lem3  15788  lgsdir  15793  lgsdilem2  15794  lgsdi  15795  lgsne0  15796  lgsprme0  15800  lgsdirnn0  15805  lgsdinn0  15806  usgrexmpldifpr  16129  vdegp1bid  16195  wlkv0  16249  wlklenvclwlk  16253  upgr2wlkdc  16257  clwwlkccatlem  16280  eupthfi  16331  trlsegvdeglem6  16345  konigsbergvtx  16362  konigsbergiedg  16363  konigsbergumgr  16367  konigsberglem1  16368  konigsberglem2  16369  konigsberglem3  16370  konigsberglem5  16372  konigsberg  16373  apdifflemr  16718  apdiff  16719  qdiff  16720  iswomni0  16723  nconstwlpolem  16737