Theorem 0z 9667

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 8333	. 2 ⊢ 0 ∈ ℝ
2		eqid 2238	. . 3 ⊢ 0 = 0
3	2	3mix1i 1200	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 9658	. 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 8185  0cc0 8186   -cneg 8506  ℕcn 9314  ℤcz 9656

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 8280  ax-addrcl 8283  ax-rnegex 8295

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 4132  df-iota 5340  df-fv 5388  df-ov 6091  df-neg 8508  df-z 9657

This theorem is used by:  0zd  9668  nn0ssz  9674  znegcl  9687  nnnle0  9705  zgt0ge1  9715  nn0n0n1ge2b  9737  nn0lt10b  9738  nnm1ge0  9744  gtndiv  9753  msqznn  9758  zeo  9763  nn0ind  9772  fnn0ind  9774  nn0uz  9974  1eluzge0  9991  elnn0dc  10028  eqreznegel  10031  qreccl  10059  qdivcl  10060  irrmul  10065  irrmulap  10066  fz10  10468  fz00m1  10469  fz01en  10477  fzpreddisj  10496  fzshftral  10533  fznn0  10538  fz1ssfz0  10542  fz0sn  10546  fz0tp  10547  fz0to3un2pr  10548  fz0to4untppr  10549  elfz0ubfz0  10550  1fv  10564  fzo0n  10593  lbfzo0  10610  elfzonlteqm1  10646  fzo01  10652  fzo0to2pr  10654  fzo0to3tp  10655  flqge0nn0  10750  divfl0  10753  btwnzge0  10757  modqmulnn  10801  zmodfz  10805  modqid  10808  zmodid2  10811  q0mod  10814  modqmuladdnn0  10827  frecfzennn  10885  xnn0nnen  10896  qexpclz  11019  qsqeqor  11109  facdiv  11199  bcval  11210  bcnn  11218  bcm1k  11221  bcval5  11224  bcpasc  11227  4bc2eq6  11236  hashinfom  11240  hashfibc  11306  iswrd  11329  iswrdiz  11334  wrdexg  11338  wrdfin  11346  wrdnval  11358  wrdred1hash  11371  lsw0  11375  ccatsymb  11393  ccatalpha  11404  s111  11422  ccat1st1st  11432  fzowrddc  11442  swrdlen  11447  swrdnd  11454  swrdwrdsymbg  11459  swrds1  11463  pfxval  11469  pfx00g  11470  pfx0g  11471  fnpfx  11472  pfxlen  11480  swrdccatin1  11520  swrdccat  11530  swrdccat3blem  11534  rexfiuz  11778  qabsor  11864  nn0abscl  11875  nnabscl  11890  climz  12084  climaddc1  12121  climmulc2  12123  climsubc1  12124  climsubc2  12125  climlec2  12133  binomlem  12276  binom  12277  bcxmas  12282  arisum2  12292  explecnv  12298  ef0lem  12453  dvdsval2  12583  dvdsdc  12591  moddvds  12592  dvds0  12599  0dvds  12604  zdvdsdc  12605  dvdscmulr  12613  dvdsmulcr  12614  fsumdvds  12635  dvdslelemd  12636  dvdsabseq  12640  divconjdvds  12642  alzdvds  12647  fzo0dvdseq  12650  odd2np1lem  12665  bitsfzo  12748  bitsmod  12749  0bits  12752  m1bits  12753  bitsinv1lem  12754  bitsinv1  12755  gcdmndc  12758  gcdsupex  12760  gcdsupcl  12761  gcd0val  12763  gcddvds  12766  gcd0id  12782  gcdid0  12783  gcdid  12789  bezoutlema  12802  bezoutlemb  12803  bezoutlembi  12808  dfgcd3  12813  dfgcd2  12817  gcdmultiplez  12824  dvdssq  12834  algcvgblem  12853  lcmmndc  12866  lcm0val  12869  dvdslcm  12873  lcmeq0  12875  lcmgcd  12882  lcmdvds  12883  lcmid  12884  3lcm2e6woprm  12890  6lcm4e12  12891  cncongr2  12908  sqrt2irrap  12986  sqrtrirr  13015  dfphi2  13028  phiprmpw  13030  crth  13032  phimullem  13033  eulerthlemfi  13036  hashgcdeq  13048  phisum  13049  pceu  13104  pcdiv  13111  pc0  13113  pcqdiv  13116  pcexp  13118  pcxnn0cl  13119  pcxcl  13120  pcxqcl  13121  pcdvdstr  13136  dvdsprmpweqnn  13145  pcaddlem  13148  pcadd  13149  pcfaclem  13158  qexpz  13161  zgz  13182  igz  13183  4sqlem19  13218  1259lem1  13272  1259lem4  13275  ballotfilemonn  13280  ballotfilem2  13287  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemefi  13296  ballotfilemodife  13299  ballotfilemscl  13306  ballotfilemsle  13307  ennnfonelemjn  13352  ennnfonelem1  13357  mulg0  13988  subgmulg  14051  zring0  15045  zndvds0  15095  znf1o  15096  znfi  15100  znhash  15101  psr1clfi  15203  plycolemc  15996  rpcxp0  16143  0sgm  16266  ppiqltx  16293  1sgmprm  16300  ppiqub  16305  bcmono  16316  bposlem1  16323  bposlem2  16324  lgslem2  16337  lgsfcl2  16342  lgs0  16349  lgsneg  16360  lgsdilem  16363  lgsdir2lem3  16366  lgsdir  16371  lgsdilem2  16372  lgsdi  16373  lgsne0  16374  lgsprme0  16378  lgsdirnn0  16383  lgsdinn0  16384  usgrexmpldifpr  16707  vdegp1bid  16773  wlkv0  16827  wlklenvclwlk  16831  upgr2wlkdc  16835  clwwlkccatlem  16858  eupthfi  16909  trlsegvdeglem6  16923  konigsbergvtx  16940  konigsbergiedg  16941  konigsbergumgr  16945  konigsberglem1  16946  konigsberglem2  16947  konigsberglem3  16948  konigsberglem5  16950  konigsberg  16951  apdifflemr  17315  apdiff  17316  qdiff  17317  iswomni0  17320  nconstwlpolem  17334