Theorem 0z 9638

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

Syntax hints:   ∨ w3o 1008   = wceq 1402   ∈ wcel 2209  ℝcr 8172  0cc0 8173  -cneg 8492  ℕcn 9287  ℤcz 9627

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 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 8267  ax-addrcl 8270  ax-rnegex 8282

This theorem 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 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-iota 5335  df-fv 5383  df-ov 6082  df-neg 8494  df-z 9628

This theorem is referenced by:  0zd  9639  nn0ssz  9645  znegcl  9658  nnnle0  9676  zgt0ge1  9686  nn0n0n1ge2b  9708  nn0lt10b  9709  nnm1ge0  9715  gtndiv  9724  msqznn  9729  zeo  9734  nn0ind  9743  fnn0ind  9745  nn0uz  9940  1eluzge0  9957  elnn0dc  9994  eqreznegel  9997  qreccl  10025  qdivcl  10026  irrmul  10030  irrmulap  10031  fz10  10433  fz00m1  10434  fz01en  10442  fzpreddisj  10461  fzshftral  10498  fznn0  10503  fz1ssfz0  10507  fz0sn  10511  fz0tp  10512  fz0to3un2pr  10513  fz0to4untppr  10514  elfz0ubfz0  10515  1fv  10529  fzo0n  10558  lbfzo0  10575  elfzonlteqm1  10611  fzo01  10617  fzo0to2pr  10619  fzo0to3tp  10620  flqge0nn0  10711  divfl0  10714  btwnzge0  10718  modqmulnn  10762  zmodfz  10766  modqid  10769  zmodid2  10772  q0mod  10775  modqmuladdnn0  10788  frecfzennn  10846  xnn0nnen  10857  qexpclz  10980  qsqeqor  11070  facdiv  11159  bcval  11170  bcnn  11178  bcm1k  11181  bcval5  11184  bcpasc  11187  4bc2eq6  11196  hashinfom  11200  hashfibc  11266  iswrd  11289  iswrdiz  11294  wrdexg  11298  wrdfin  11306  wrdnval  11318  wrdred1hash  11331  lsw0  11335  ccatsymb  11353  ccatalpha  11364  s111  11382  ccat1st1st  11392  fzowrddc  11402  swrdlen  11407  swrdnd  11414  swrdwrdsymbg  11419  swrds1  11423  pfxval  11429  pfx00g  11430  pfx0g  11431  fnpfx  11432  pfxlen  11440  swrdccatin1  11480  swrdccat  11490  swrdccat3blem  11494  rexfiuz  11738  qabsor  11824  nn0abscl  11834  nnabscl  11849  climz  12041  climaddc1  12078  climmulc2  12080  climsubc1  12081  climsubc2  12082  climlec2  12090  binomlem  12233  binom  12234  bcxmas  12239  arisum2  12249  explecnv  12255  ef0lem  12410  dvdsval2  12540  dvdsdc  12548  moddvds  12549  dvds0  12556  0dvds  12561  zdvdsdc  12562  dvdscmulr  12570  dvdsmulcr  12571  fsumdvds  12592  dvdslelemd  12593  dvdsabseq  12597  divconjdvds  12599  alzdvds  12604  fzo0dvdseq  12607  odd2np1lem  12622  bitsfzo  12705  bitsmod  12706  0bits  12709  m1bits  12710  bitsinv1lem  12711  bitsinv1  12712  gcdmndc  12715  gcdsupex  12717  gcdsupcl  12718  gcd0val  12720  gcddvds  12723  gcd0id  12739  gcdid0  12740  gcdid  12746  bezoutlema  12759  bezoutlemb  12760  bezoutlembi  12765  dfgcd3  12770  dfgcd2  12774  gcdmultiplez  12781  dvdssq  12791  algcvgblem  12810  lcmmndc  12823  lcm0val  12826  dvdslcm  12830  lcmeq0  12832  lcmgcd  12839  lcmdvds  12840  lcmid  12841  3lcm2e6woprm  12847  6lcm4e12  12848  cncongr2  12865  sqrt2irrap  12941  dfphi2  12981  phiprmpw  12983  crth  12985  phimullem  12986  eulerthlemfi  12989  hashgcdeq  13001  phisum  13002  pceu  13057  pcdiv  13064  pc0  13066  pcqdiv  13069  pcexp  13071  pcxnn0cl  13072  pcxcl  13073  pcxqcl  13074  pcdvdstr  13089  dvdsprmpweqnn  13098  pcaddlem  13101  pcadd  13102  pcfaclem  13111  qexpz  13114  zgz  13135  igz  13136  4sqlem19  13171  ballotfilemonn  13204  ballotfilem2  13211  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemefi  13220  ballotfilemodife  13223  ballotfilemscl  13230  ballotfilemsle  13231  ennnfonelemjn  13276  ennnfonelem1  13281  mulg0  13911  subgmulg  13974  zring0  14918  zndvds0  14968  znf1o  14969  znfi  14973  znhash  14974  psr1clfi  15062  plycolemc  15842  rpcxp0  15983  0sgm  16082  1sgmprm  16091  lgslem2  16103  lgsfcl2  16108  lgs0  16115  lgsneg  16126  lgsdilem  16129  lgsdir2lem3  16132  lgsdir  16137  lgsdilem2  16138  lgsdi  16139  lgsne0  16140  lgsprme0  16144  lgsdirnn0  16149  lgsdinn0  16150  usgrexmpldifpr  16473  vdegp1bid  16539  wlkv0  16593  wlklenvclwlk  16597  upgr2wlkdc  16601  clwwlkccatlem  16624  eupthfi  16675  trlsegvdeglem6  16689  konigsbergvtx  16706  konigsbergiedg  16707  konigsbergumgr  16711  konigsberglem1  16712  konigsberglem2  16713  konigsberglem3  16714  konigsberglem5  16716  konigsberg  16717  apdifflemr  17070  apdiff  17071  qdiff  17072  iswomni0  17075  nconstwlpolem  17089