Theorem 0z 9089

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 7790	. 2 ⊢ 0 ∈ ℝ
2		eqid 2140	. . 3 ⊢ 0 = 0
3	2	3mix1i 1154	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 9080	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 927	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 962   = wceq 1332   ∈ wcel 1481  ℝcr 7643  0cc0 7644  -cneg 7958  ℕcn 8744  ℤcz 9078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-1re 7738  ax-addrcl 7741  ax-rnegex 7753

This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-rab 2426  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139  df-ov 5785  df-neg 7960  df-z 9079

This theorem is referenced by:  0zd  9090  nn0ssz  9096  znegcl  9109  zgt0ge1  9136  nn0n0n1ge2b  9154  nn0lt10b  9155  nnm1ge0  9161  gtndiv  9170  msqznn  9175  zeo  9180  nn0ind  9189  fnn0ind  9191  nn0uz  9384  1eluzge0  9396  eqreznegel  9433  qreccl  9461  qdivcl  9462  irrmul  9466  fz10  9857  fz01en  9864  fzpreddisj  9882  fzshftral  9919  fznn0  9924  fz1ssfz0  9928  fz0tp  9932  elfz0ubfz0  9933  1fv  9947  lbfzo0  9989  elfzonlteqm1  10018  fzo01  10024  fzo0to2pr  10026  fzo0to3tp  10027  flqge0nn0  10097  divfl0  10100  btwnzge0  10104  modqmulnn  10146  zmodfz  10150  modqid  10153  zmodid2  10156  q0mod  10159  modqmuladdnn0  10172  frecfzennn  10230  qexpclz  10345  facdiv  10516  bcval  10527  bcnn  10535  bcm1k  10538  bcval5  10541  bcpasc  10544  4bc2eq6  10552  hashinfom  10556  rexfiuz  10793  qabsor  10879  nn0abscl  10889  nnabscl  10904  climz  11093  climaddc1  11130  climmulc2  11132  climsubc1  11133  climsubc2  11134  climlec2  11142  binomlem  11284  binom  11285  bcxmas  11290  arisum2  11300  explecnv  11306  ef0lem  11403  dvdsval2  11532  dvdsdc  11537  moddvds  11538  dvds0  11544  0dvds  11549  zdvdsdc  11550  dvdscmulr  11558  dvdsmulcr  11559  dvdslelemd  11577  dvdsabseq  11581  divconjdvds  11583  alzdvds  11588  fzo0dvdseq  11591  odd2np1lem  11605  gcdmndc  11673  gcdsupex  11682  gcdsupcl  11683  gcd0val  11685  gcddvds  11688  gcd0id  11703  gcdid0  11704  gcdid  11710  bezoutlema  11723  bezoutlemb  11724  bezoutlembi  11729  dfgcd3  11734  dfgcd2  11738  gcdmultiplez  11745  dvdssq  11755  algcvgblem  11766  lcmmndc  11779  lcm0val  11782  dvdslcm  11786  lcmeq0  11788  lcmgcd  11795  lcmdvds  11796  lcmid  11797  3lcm2e6woprm  11803  6lcm4e12  11804  cncongr2  11821  sqrt2irrap  11894  dfphi2  11932  phiprmpw  11934  crth  11936  phimullem  11937  hashgcdeq  11940  ennnfonelemjn  11951  ennnfonelem1  11956  rpcxp0  13027  apdifflemr  13415  apdiff  13416