Theorem 0z 9465

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

Syntax hints:   ∨ w3o 1001   = wceq 1395   ∈ wcel 2200  ℝcr 8006  0cc0 8007  -cneg 8326  ℕcn 9118  ℤcz 9454

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 8101  ax-addrcl 8104  ax-rnegex 8116

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 5278  df-fv 5326  df-ov 6010  df-neg 8328  df-z 9455

This theorem is referenced by:  0zd  9466  nn0ssz  9472  znegcl  9485  nnnle0  9503  zgt0ge1  9513  nn0n0n1ge2b  9534  nn0lt10b  9535  nnm1ge0  9541  gtndiv  9550  msqznn  9555  zeo  9560  nn0ind  9569  fnn0ind  9571  nn0uz  9765  1eluzge0  9777  elnn0dc  9814  eqreznegel  9817  qreccl  9845  qdivcl  9846  irrmul  9850  irrmulap  9851  fz10  10250  fz01en  10257  fzpreddisj  10275  fzshftral  10312  fznn0  10317  fz1ssfz0  10321  fz0sn  10325  fz0tp  10326  fz0to3un2pr  10327  fz0to4untppr  10328  elfz0ubfz0  10329  1fv  10343  fzo0n  10372  lbfzo0  10389  elfzonlteqm1  10424  fzo01  10430  fzo0to2pr  10432  fzo0to3tp  10433  flqge0nn0  10521  divfl0  10524  btwnzge0  10528  modqmulnn  10572  zmodfz  10576  modqid  10579  zmodid2  10582  q0mod  10585  modqmuladdnn0  10598  frecfzennn  10656  xnn0nnen  10667  qexpclz  10790  qsqeqor  10880  facdiv  10968  bcval  10979  bcnn  10987  bcm1k  10990  bcval5  10993  bcpasc  10996  4bc2eq6  11004  hashinfom  11008  iswrd  11081  iswrdiz  11086  wrdexg  11090  wrdfin  11098  wrdnval  11110  wrdred1hash  11123  lsw0  11127  ccatsymb  11145  s111  11172  ccat1st1st  11180  fzowrddc  11187  swrdlen  11192  swrdnd  11199  swrdwrdsymbg  11204  swrds1  11208  pfxval  11214  pfx00g  11215  pfx0g  11216  fnpfx  11217  pfxlen  11225  swrdccatin1  11265  swrdccat  11275  swrdccat3blem  11279  rexfiuz  11508  qabsor  11594  nn0abscl  11604  nnabscl  11619  climz  11811  climaddc1  11848  climmulc2  11850  climsubc1  11851  climsubc2  11852  climlec2  11860  binomlem  12002  binom  12003  bcxmas  12008  arisum2  12018  explecnv  12024  ef0lem  12179  dvdsval2  12309  dvdsdc  12317  moddvds  12318  dvds0  12325  0dvds  12330  zdvdsdc  12331  dvdscmulr  12339  dvdsmulcr  12340  fsumdvds  12361  dvdslelemd  12362  dvdsabseq  12366  divconjdvds  12368  alzdvds  12373  fzo0dvdseq  12376  odd2np1lem  12391  bitsfzo  12474  bitsmod  12475  0bits  12478  m1bits  12479  bitsinv1lem  12480  bitsinv1  12481  gcdmndc  12484  gcdsupex  12486  gcdsupcl  12487  gcd0val  12489  gcddvds  12492  gcd0id  12508  gcdid0  12509  gcdid  12515  bezoutlema  12528  bezoutlemb  12529  bezoutlembi  12534  dfgcd3  12539  dfgcd2  12543  gcdmultiplez  12550  dvdssq  12560  algcvgblem  12579  lcmmndc  12592  lcm0val  12595  dvdslcm  12599  lcmeq0  12601  lcmgcd  12608  lcmdvds  12609  lcmid  12610  3lcm2e6woprm  12616  6lcm4e12  12617  cncongr2  12634  sqrt2irrap  12710  dfphi2  12750  phiprmpw  12752  crth  12754  phimullem  12755  eulerthlemfi  12758  hashgcdeq  12770  phisum  12771  pceu  12826  pcdiv  12833  pc0  12835  pcqdiv  12838  pcexp  12840  pcxnn0cl  12841  pcxcl  12842  pcxqcl  12843  pcdvdstr  12858  dvdsprmpweqnn  12867  pcaddlem  12870  pcadd  12871  pcfaclem  12880  qexpz  12883  zgz  12904  igz  12905  4sqlem19  12940  ennnfonelemjn  12981  ennnfonelem1  12986  mulg0  13670  subgmulg  13733  zring0  14572  zndvds0  14622  znf1o  14623  znfi  14627  znhash  14628  psr1clfi  14660  plycolemc  15440  rpcxp0  15580  0sgm  15667  1sgmprm  15676  lgslem2  15688  lgsfcl2  15693  lgs0  15700  lgsneg  15711  lgsdilem  15714  lgsdir2lem3  15717  lgsdir  15722  lgsdilem2  15723  lgsdi  15724  lgsne0  15725  lgsprme0  15729  lgsdirnn0  15734  lgsdinn0  15735  wlkv0  16090  wlklenvclwlk  16094  upgr2wlkdc  16096  apdifflemr  16445  apdiff  16446  iswomni0  16449  nconstwlpolem  16463