Theorem 0z 9590

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

Syntax hints:   ∨ w3o 1004   = wceq 1398   ∈ wcel 2205  ℝcr 8128  0cc0 8129  -cneg 8447  ℕcn 9239  ℤcz 9579

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 8223  ax-addrcl 8226  ax-rnegex 8238

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 8449  df-z 9580

This theorem is referenced by:  0zd  9591  nn0ssz  9597  znegcl  9610  nnnle0  9628  zgt0ge1  9638  nn0n0n1ge2b  9660  nn0lt10b  9661  nnm1ge0  9667  gtndiv  9676  msqznn  9681  zeo  9686  nn0ind  9695  fnn0ind  9697  nn0uz  9892  1eluzge0  9909  elnn0dc  9946  eqreznegel  9949  qreccl  9977  qdivcl  9978  irrmul  9982  irrmulap  9983  fz10  10383  fz01en  10390  fzpreddisj  10409  fzshftral  10446  fznn0  10451  fz1ssfz0  10455  fz0sn  10459  fz0tp  10460  fz0to3un2pr  10461  fz0to4untppr  10462  elfz0ubfz0  10463  1fv  10477  fzo0n  10506  lbfzo0  10523  elfzonlteqm1  10559  fzo01  10565  fzo0to2pr  10567  fzo0to3tp  10568  flqge0nn0  10657  divfl0  10660  btwnzge0  10664  modqmulnn  10708  zmodfz  10712  modqid  10715  zmodid2  10718  q0mod  10721  modqmuladdnn0  10734  frecfzennn  10792  xnn0nnen  10803  qexpclz  10926  qsqeqor  11016  facdiv  11104  bcval  11115  bcnn  11123  bcm1k  11126  bcval5  11129  bcpasc  11132  4bc2eq6  11141  hashinfom  11145  hashfibc  11211  iswrd  11230  iswrdiz  11235  wrdexg  11239  wrdfin  11247  wrdnval  11259  wrdred1hash  11272  lsw0  11276  ccatsymb  11294  ccatalpha  11305  s111  11323  ccat1st1st  11333  fzowrddc  11343  swrdlen  11348  swrdnd  11355  swrdwrdsymbg  11360  swrds1  11364  pfxval  11370  pfx00g  11371  pfx0g  11372  fnpfx  11373  pfxlen  11381  swrdccatin1  11421  swrdccat  11431  swrdccat3blem  11435  rexfiuz  11678  qabsor  11764  nn0abscl  11774  nnabscl  11789  climz  11981  climaddc1  12018  climmulc2  12020  climsubc1  12021  climsubc2  12022  climlec2  12030  binomlem  12173  binom  12174  bcxmas  12179  arisum2  12189  explecnv  12195  ef0lem  12350  dvdsval2  12480  dvdsdc  12488  moddvds  12489  dvds0  12496  0dvds  12501  zdvdsdc  12502  dvdscmulr  12510  dvdsmulcr  12511  fsumdvds  12532  dvdslelemd  12533  dvdsabseq  12537  divconjdvds  12539  alzdvds  12544  fzo0dvdseq  12547  odd2np1lem  12562  bitsfzo  12645  bitsmod  12646  0bits  12649  m1bits  12650  bitsinv1lem  12651  bitsinv1  12652  gcdmndc  12655  gcdsupex  12657  gcdsupcl  12658  gcd0val  12660  gcddvds  12663  gcd0id  12679  gcdid0  12680  gcdid  12686  bezoutlema  12699  bezoutlemb  12700  bezoutlembi  12705  dfgcd3  12710  dfgcd2  12714  gcdmultiplez  12721  dvdssq  12731  algcvgblem  12750  lcmmndc  12763  lcm0val  12766  dvdslcm  12770  lcmeq0  12772  lcmgcd  12779  lcmdvds  12780  lcmid  12781  3lcm2e6woprm  12787  6lcm4e12  12788  cncongr2  12805  sqrt2irrap  12881  dfphi2  12921  phiprmpw  12923  crth  12925  phimullem  12926  eulerthlemfi  12929  hashgcdeq  12941  phisum  12942  pceu  12997  pcdiv  13004  pc0  13006  pcqdiv  13009  pcexp  13011  pcxnn0cl  13012  pcxcl  13013  pcxqcl  13014  pcdvdstr  13029  dvdsprmpweqnn  13038  pcaddlem  13041  pcadd  13042  pcfaclem  13051  qexpz  13054  zgz  13075  igz  13076  4sqlem19  13111  ballotfilemonn  13144  ballotfilem2  13149  ballotfilemfc0  13153  ballotfilemfcc  13154  ballotfilemodife  13158  ennnfonelemjn  13170  ennnfonelem1  13175  mulg0  13859  subgmulg  13922  zring0  14765  zndvds0  14815  znf1o  14816  znfi  14820  znhash  14821  psr1clfi  14860  plycolemc  15640  rpcxp0  15780  0sgm  15870  1sgmprm  15879  lgslem2  15891  lgsfcl2  15896  lgs0  15903  lgsneg  15914  lgsdilem  15917  lgsdir2lem3  15920  lgsdir  15925  lgsdilem2  15926  lgsdi  15927  lgsne0  15928  lgsprme0  15932  lgsdirnn0  15937  lgsdinn0  15938  usgrexmpldifpr  16261  vdegp1bid  16327  wlkv0  16381  wlklenvclwlk  16385  upgr2wlkdc  16389  clwwlkccatlem  16412  eupthfi  16463  trlsegvdeglem6  16477  konigsbergvtx  16494  konigsbergiedg  16495  konigsbergumgr  16499  konigsberglem1  16500  konigsberglem2  16501  konigsberglem3  16502  konigsberglem5  16504  konigsberg  16505  apdifflemr  16848  apdiff  16849  qdiff  16850  iswomni0  16853  nconstwlpolem  16868