Theorem 0z 9660

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 8327	. 2 ⊢ 0 ∈ ℝ
2		eqid 2238	. . 3 ⊢ 0 = 0
3	2	3mix1i 1200	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 9651	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 955	1 ⊢ 0 ∈ ℤ

This proof depends on syntax axioms:   ∨ w3o 1008   = wceq 1402   ∈ wcel 2209  ℝcr 8179  0cc0 8180  -cneg 8500  ℕcn 9307  ℤcz 9649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1re 8274  ax-addrcl 8277  ax-rnegex 8289

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-rab 2537  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088  df-neg 8502  df-z 9650

This theorem is used by:  0zd  9661  nn0ssz  9667  znegcl  9680  nnnle0  9698  zgt0ge1  9708  nn0n0n1ge2b  9730  nn0lt10b  9731  nnm1ge0  9737  gtndiv  9746  msqznn  9751  zeo  9756  nn0ind  9765  fnn0ind  9767  nn0uz  9967  1eluzge0  9984  elnn0dc  10021  eqreznegel  10024  qreccl  10052  qdivcl  10053  irrmul  10058  irrmulap  10059  fz10  10461  fz00m1  10462  fz01en  10470  fzpreddisj  10489  fzshftral  10526  fznn0  10531  fz1ssfz0  10535  fz0sn  10539  fz0tp  10540  fz0to3un2pr  10541  fz0to4untppr  10542  elfz0ubfz0  10543  1fv  10557  fzo0n  10586  lbfzo0  10603  elfzonlteqm1  10639  fzo01  10645  fzo0to2pr  10647  fzo0to3tp  10648  flqge0nn0  10743  divfl0  10746  btwnzge0  10750  modqmulnn  10794  zmodfz  10798  modqid  10801  zmodid2  10804  q0mod  10807  modqmuladdnn0  10820  frecfzennn  10878  xnn0nnen  10889  qexpclz  11012  qsqeqor  11102  facdiv  11192  bcval  11203  bcnn  11211  bcm1k  11214  bcval5  11217  bcpasc  11220  4bc2eq6  11229  hashinfom  11233  hashfibc  11299  iswrd  11322  iswrdiz  11327  wrdexg  11331  wrdfin  11339  wrdnval  11351  wrdred1hash  11364  lsw0  11368  ccatsymb  11386  ccatalpha  11397  s111  11415  ccat1st1st  11425  fzowrddc  11435  swrdlen  11440  swrdnd  11447  swrdwrdsymbg  11452  swrds1  11456  pfxval  11462  pfx00g  11463  pfx0g  11464  fnpfx  11465  pfxlen  11473  swrdccatin1  11513  swrdccat  11523  swrdccat3blem  11527  rexfiuz  11771  qabsor  11857  nn0abscl  11868  nnabscl  11883  climz  12077  climaddc1  12114  climmulc2  12116  climsubc1  12117  climsubc2  12118  climlec2  12126  binomlem  12269  binom  12270  bcxmas  12275  arisum2  12285  explecnv  12291  ef0lem  12446  dvdsval2  12576  dvdsdc  12584  moddvds  12585  dvds0  12592  0dvds  12597  zdvdsdc  12598  dvdscmulr  12606  dvdsmulcr  12607  fsumdvds  12628  dvdslelemd  12629  dvdsabseq  12633  divconjdvds  12635  alzdvds  12640  fzo0dvdseq  12643  odd2np1lem  12658  bitsfzo  12741  bitsmod  12742  0bits  12745  m1bits  12746  bitsinv1lem  12747  bitsinv1  12748  gcdmndc  12751  gcdsupex  12753  gcdsupcl  12754  gcd0val  12756  gcddvds  12759  gcd0id  12775  gcdid0  12776  gcdid  12782  bezoutlema  12795  bezoutlemb  12796  bezoutlembi  12801  dfgcd3  12806  dfgcd2  12810  gcdmultiplez  12817  dvdssq  12827  algcvgblem  12846  lcmmndc  12859  lcm0val  12862  dvdslcm  12866  lcmeq0  12868  lcmgcd  12875  lcmdvds  12876  lcmid  12877  3lcm2e6woprm  12883  6lcm4e12  12884  cncongr2  12901  sqrt2irrap  12979  sqrtrirr  13008  dfphi2  13021  phiprmpw  13023  crth  13025  phimullem  13026  eulerthlemfi  13029  hashgcdeq  13041  phisum  13042  pceu  13097  pcdiv  13104  pc0  13106  pcqdiv  13109  pcexp  13111  pcxnn0cl  13112  pcxcl  13113  pcxqcl  13114  pcdvdstr  13129  dvdsprmpweqnn  13138  pcaddlem  13141  pcadd  13142  pcfaclem  13151  qexpz  13154  zgz  13175  igz  13176  4sqlem19  13211  1259lem1  13265  1259lem4  13268  ballotfilemonn  13273  ballotfilem2  13280  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemefi  13289  ballotfilemodife  13292  ballotfilemscl  13299  ballotfilemsle  13300  ennnfonelemjn  13345  ennnfonelem1  13350  mulg0  13981  subgmulg  14044  zring0  15019  zndvds0  15069  znf1o  15070  znfi  15074  znhash  15075  psr1clfi  15170  plycolemc  15950  rpcxp0  16097  0sgm  16220  ppiqltx  16247  1sgmprm  16254  ppiqub  16259  bcmono  16270  bposlem1  16277  bposlem2  16278  lgslem2  16291  lgsfcl2  16296  lgs0  16303  lgsneg  16314  lgsdilem  16317  lgsdir2lem3  16320  lgsdir  16325  lgsdilem2  16326  lgsdi  16327  lgsne0  16328  lgsprme0  16332  lgsdirnn0  16337  lgsdinn0  16338  usgrexmpldifpr  16661  vdegp1bid  16727  wlkv0  16781  wlklenvclwlk  16785  upgr2wlkdc  16789  clwwlkccatlem  16812  eupthfi  16863  trlsegvdeglem6  16877  konigsbergvtx  16894  konigsbergiedg  16895  konigsbergumgr  16899  konigsberglem1  16900  konigsberglem2  16901  konigsberglem3  16902  konigsberglem5  16904  konigsberg  16905  apdifflemr  17268  apdiff  17269  qdiff  17270  iswomni0  17273  nconstwlpolem  17287