Theorem 0z 9065

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 7766	. 2 ⊢ 0 ∈ ℝ
2		eqid 2139	. . 3 ⊢ 0 = 0
3	2	3mix1i 1153	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 9056	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 926	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 961   = wceq 1331   ∈ wcel 1480  ℝcr 7619  0cc0 7620  -cneg 7934  ℕcn 8720  ℤcz 9054

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-1re 7714  ax-addrcl 7717  ax-rnegex 7729

This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-rab 2425  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-iota 5088  df-fv 5131  df-ov 5777  df-neg 7936  df-z 9055

This theorem is referenced by:  0zd  9066  nn0ssz  9072  znegcl  9085  zgt0ge1  9112  nn0n0n1ge2b  9130  nn0lt10b  9131  nnm1ge0  9137  gtndiv  9146  msqznn  9151  zeo  9156  nn0ind  9165  fnn0ind  9167  nn0uz  9360  1eluzge0  9369  eqreznegel  9406  qreccl  9434  qdivcl  9435  irrmul  9439  fz10  9826  fz01en  9833  fzpreddisj  9851  fzshftral  9888  fznn0  9893  fz1ssfz0  9897  fz0tp  9901  elfz0ubfz0  9902  1fv  9916  lbfzo0  9958  elfzonlteqm1  9987  fzo01  9993  fzo0to2pr  9995  fzo0to3tp  9996  flqge0nn0  10066  divfl0  10069  btwnzge0  10073  modqmulnn  10115  zmodfz  10119  modqid  10122  zmodid2  10125  q0mod  10128  modqmuladdnn0  10141  frecfzennn  10199  qexpclz  10314  facdiv  10484  bcval  10495  bcnn  10503  bcm1k  10506  bcval5  10509  bcpasc  10512  4bc2eq6  10520  hashinfom  10524  rexfiuz  10761  qabsor  10847  nn0abscl  10857  nnabscl  10872  climz  11061  climaddc1  11098  climmulc2  11100  climsubc1  11101  climsubc2  11102  climlec2  11110  binomlem  11252  binom  11253  bcxmas  11258  arisum2  11268  explecnv  11274  ef0lem  11366  dvdsval2  11496  dvdsdc  11501  moddvds  11502  dvds0  11508  0dvds  11513  zdvdsdc  11514  dvdscmulr  11522  dvdsmulcr  11523  dvdslelemd  11541  dvdsabseq  11545  divconjdvds  11547  alzdvds  11552  fzo0dvdseq  11555  odd2np1lem  11569  gcdmndc  11637  gcdsupex  11646  gcdsupcl  11647  gcd0val  11649  gcddvds  11652  gcd0id  11667  gcdid0  11668  gcdid  11674  bezoutlema  11687  bezoutlemb  11688  bezoutlembi  11693  dfgcd3  11698  dfgcd2  11702  gcdmultiplez  11709  dvdssq  11719  algcvgblem  11730  lcmmndc  11743  lcm0val  11746  dvdslcm  11750  lcmeq0  11752  lcmgcd  11759  lcmdvds  11760  lcmid  11761  3lcm2e6woprm  11767  6lcm4e12  11768  cncongr2  11785  sqrt2irrap  11858  dfphi2  11896  phiprmpw  11898  crth  11900  phimullem  11901  hashgcdeq  11904  ennnfonelemjn  11915  ennnfonelem1  11920