Theorem 0z 9608

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 8290	. 2 ⊢ 0 ∈ ℝ
2		eqid 2234	. . 3 ⊢ 0 = 0
3	2	3mix1i 1196	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 9599	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 951	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1004   = wceq 1398   ∈ wcel 2205  ℝcr 8142  0cc0 8143  -cneg 8462  ℕcn 9257  ℤcz 9597

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-1re 8237  ax-addrcl 8240  ax-rnegex 8252

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-rab 2531  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061  df-neg 8464  df-z 9598

This theorem is referenced by:  0zd  9609  nn0ssz  9615  znegcl  9628  nnnle0  9646  zgt0ge1  9656  nn0n0n1ge2b  9678  nn0lt10b  9679  nnm1ge0  9685  gtndiv  9694  msqznn  9699  zeo  9704  nn0ind  9713  fnn0ind  9715  nn0uz  9910  1eluzge0  9927  elnn0dc  9964  eqreznegel  9967  qreccl  9995  qdivcl  9996  irrmul  10000  irrmulap  10001  fz10  10403  fz01en  10411  fzpreddisj  10430  fzshftral  10467  fznn0  10472  fz1ssfz0  10476  fz0sn  10480  fz0tp  10481  fz0to3un2pr  10482  fz0to4untppr  10483  elfz0ubfz0  10484  1fv  10498  fzo0n  10527  lbfzo0  10544  elfzonlteqm1  10580  fzo01  10586  fzo0to2pr  10588  fzo0to3tp  10589  flqge0nn0  10680  divfl0  10683  btwnzge0  10687  modqmulnn  10731  zmodfz  10735  modqid  10738  zmodid2  10741  q0mod  10744  modqmuladdnn0  10757  frecfzennn  10815  xnn0nnen  10826  qexpclz  10949  qsqeqor  11039  facdiv  11128  bcval  11139  bcnn  11147  bcm1k  11150  bcval5  11153  bcpasc  11156  4bc2eq6  11165  hashinfom  11169  hashfibc  11235  iswrd  11254  iswrdiz  11259  wrdexg  11263  wrdfin  11271  wrdnval  11283  wrdred1hash  11296  lsw0  11300  ccatsymb  11318  ccatalpha  11329  s111  11347  ccat1st1st  11357  fzowrddc  11367  swrdlen  11372  swrdnd  11379  swrdwrdsymbg  11384  swrds1  11388  pfxval  11394  pfx00g  11395  pfx0g  11396  fnpfx  11397  pfxlen  11405  swrdccatin1  11445  swrdccat  11455  swrdccat3blem  11459  rexfiuz  11702  qabsor  11788  nn0abscl  11798  nnabscl  11813  climz  12005  climaddc1  12042  climmulc2  12044  climsubc1  12045  climsubc2  12046  climlec2  12054  binomlem  12197  binom  12198  bcxmas  12203  arisum2  12213  explecnv  12219  ef0lem  12374  dvdsval2  12504  dvdsdc  12512  moddvds  12513  dvds0  12520  0dvds  12525  zdvdsdc  12526  dvdscmulr  12534  dvdsmulcr  12535  fsumdvds  12556  dvdslelemd  12557  dvdsabseq  12561  divconjdvds  12563  alzdvds  12568  fzo0dvdseq  12571  odd2np1lem  12586  bitsfzo  12669  bitsmod  12670  0bits  12673  m1bits  12674  bitsinv1lem  12675  bitsinv1  12676  gcdmndc  12679  gcdsupex  12681  gcdsupcl  12682  gcd0val  12684  gcddvds  12687  gcd0id  12703  gcdid0  12704  gcdid  12710  bezoutlema  12723  bezoutlemb  12724  bezoutlembi  12729  dfgcd3  12734  dfgcd2  12738  gcdmultiplez  12745  dvdssq  12755  algcvgblem  12774  lcmmndc  12787  lcm0val  12790  dvdslcm  12794  lcmeq0  12796  lcmgcd  12803  lcmdvds  12804  lcmid  12805  3lcm2e6woprm  12811  6lcm4e12  12812  cncongr2  12829  sqrt2irrap  12905  dfphi2  12945  phiprmpw  12947  crth  12949  phimullem  12950  eulerthlemfi  12953  hashgcdeq  12965  phisum  12966  pceu  13021  pcdiv  13028  pc0  13030  pcqdiv  13033  pcexp  13035  pcxnn0cl  13036  pcxcl  13037  pcxqcl  13038  pcdvdstr  13053  dvdsprmpweqnn  13062  pcaddlem  13065  pcadd  13066  pcfaclem  13075  qexpz  13078  zgz  13099  igz  13100  4sqlem19  13135  ballotfilemonn  13168  ballotfilem2  13175  ballotfilemfc0  13179  ballotfilemfcc  13180  ballotfilemefi  13184  ballotfilemodife  13187  ballotfilemscl  13194  ballotfilemsle  13195  ennnfonelemjn  13240  ennnfonelem1  13245  mulg0  13881  subgmulg  13944  zring0  14877  zndvds0  14927  znf1o  14928  znfi  14932  znhash  14933  psr1clfi  14972  plycolemc  15752  rpcxp0  15892  0sgm  15982  1sgmprm  15991  lgslem2  16003  lgsfcl2  16008  lgs0  16015  lgsneg  16026  lgsdilem  16029  lgsdir2lem3  16032  lgsdir  16037  lgsdilem2  16038  lgsdi  16039  lgsne0  16040  lgsprme0  16044  lgsdirnn0  16049  lgsdinn0  16050  usgrexmpldifpr  16373  vdegp1bid  16439  wlkv0  16493  wlklenvclwlk  16497  upgr2wlkdc  16501  clwwlkccatlem  16524  eupthfi  16575  trlsegvdeglem6  16589  konigsbergvtx  16606  konigsbergiedg  16607  konigsbergumgr  16611  konigsberglem1  16612  konigsberglem2  16613  konigsberglem3  16614  konigsberglem5  16616  konigsberg  16617  apdifflemr  16970  apdiff  16971  qdiff  16972  iswomni0  16975  nconstwlpolem  16990