Theorem 0z 9473

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

Syntax hints:   ∨ w3o 1001   = wceq 1395   ∈ wcel 2200  ℝcr 8014  0cc0 8015  -cneg 8334  ℕcn 9126  ℤcz 9462

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 8109  ax-addrcl 8112  ax-rnegex 8124

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 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5281  df-fv 5329  df-ov 6013  df-neg 8336  df-z 9463

This theorem is referenced by:  0zd  9474  nn0ssz  9480  znegcl  9493  nnnle0  9511  zgt0ge1  9521  nn0n0n1ge2b  9542  nn0lt10b  9543  nnm1ge0  9549  gtndiv  9558  msqznn  9563  zeo  9568  nn0ind  9577  fnn0ind  9579  nn0uz  9774  1eluzge0  9786  elnn0dc  9823  eqreznegel  9826  qreccl  9854  qdivcl  9855  irrmul  9859  irrmulap  9860  fz10  10259  fz01en  10266  fzpreddisj  10284  fzshftral  10321  fznn0  10326  fz1ssfz0  10330  fz0sn  10334  fz0tp  10335  fz0to3un2pr  10336  fz0to4untppr  10337  elfz0ubfz0  10338  1fv  10352  fzo0n  10381  lbfzo0  10398  elfzonlteqm1  10433  fzo01  10439  fzo0to2pr  10441  fzo0to3tp  10442  flqge0nn0  10530  divfl0  10533  btwnzge0  10537  modqmulnn  10581  zmodfz  10585  modqid  10588  zmodid2  10591  q0mod  10594  modqmuladdnn0  10607  frecfzennn  10665  xnn0nnen  10676  qexpclz  10799  qsqeqor  10889  facdiv  10977  bcval  10988  bcnn  10996  bcm1k  10999  bcval5  11002  bcpasc  11005  4bc2eq6  11013  hashinfom  11017  iswrd  11091  iswrdiz  11096  wrdexg  11100  wrdfin  11108  wrdnval  11120  wrdred1hash  11133  lsw0  11137  ccatsymb  11155  ccatalpha  11166  s111  11184  ccat1st1st  11193  fzowrddc  11200  swrdlen  11205  swrdnd  11212  swrdwrdsymbg  11217  swrds1  11221  pfxval  11227  pfx00g  11228  pfx0g  11229  fnpfx  11230  pfxlen  11238  swrdccatin1  11278  swrdccat  11288  swrdccat3blem  11292  rexfiuz  11521  qabsor  11607  nn0abscl  11617  nnabscl  11632  climz  11824  climaddc1  11861  climmulc2  11863  climsubc1  11864  climsubc2  11865  climlec2  11873  binomlem  12015  binom  12016  bcxmas  12021  arisum2  12031  explecnv  12037  ef0lem  12192  dvdsval2  12322  dvdsdc  12330  moddvds  12331  dvds0  12338  0dvds  12343  zdvdsdc  12344  dvdscmulr  12352  dvdsmulcr  12353  fsumdvds  12374  dvdslelemd  12375  dvdsabseq  12379  divconjdvds  12381  alzdvds  12386  fzo0dvdseq  12389  odd2np1lem  12404  bitsfzo  12487  bitsmod  12488  0bits  12491  m1bits  12492  bitsinv1lem  12493  bitsinv1  12494  gcdmndc  12497  gcdsupex  12499  gcdsupcl  12500  gcd0val  12502  gcddvds  12505  gcd0id  12521  gcdid0  12522  gcdid  12528  bezoutlema  12541  bezoutlemb  12542  bezoutlembi  12547  dfgcd3  12552  dfgcd2  12556  gcdmultiplez  12563  dvdssq  12573  algcvgblem  12592  lcmmndc  12605  lcm0val  12608  dvdslcm  12612  lcmeq0  12614  lcmgcd  12621  lcmdvds  12622  lcmid  12623  3lcm2e6woprm  12629  6lcm4e12  12630  cncongr2  12647  sqrt2irrap  12723  dfphi2  12763  phiprmpw  12765  crth  12767  phimullem  12768  eulerthlemfi  12771  hashgcdeq  12783  phisum  12784  pceu  12839  pcdiv  12846  pc0  12848  pcqdiv  12851  pcexp  12853  pcxnn0cl  12854  pcxcl  12855  pcxqcl  12856  pcdvdstr  12871  dvdsprmpweqnn  12880  pcaddlem  12883  pcadd  12884  pcfaclem  12893  qexpz  12896  zgz  12917  igz  12918  4sqlem19  12953  ennnfonelemjn  12994  ennnfonelem1  12999  mulg0  13683  subgmulg  13746  zring0  14585  zndvds0  14635  znf1o  14636  znfi  14640  znhash  14641  psr1clfi  14673  plycolemc  15453  rpcxp0  15593  0sgm  15680  1sgmprm  15689  lgslem2  15701  lgsfcl2  15706  lgs0  15713  lgsneg  15724  lgsdilem  15727  lgsdir2lem3  15730  lgsdir  15735  lgsdilem2  15736  lgsdi  15737  lgsne0  15738  lgsprme0  15742  lgsdirnn0  15747  lgsdinn0  15748  usgrexmpldifpr  16068  wlkv0  16141  wlklenvclwlk  16145  upgr2wlkdc  16147  clwwlkccatlem  16169  apdifflemr  16529  apdiff  16530  iswomni0  16533  nconstwlpolem  16547