Theorem 0z 8697

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 7435	. 2 ⊢ 0 ∈ ℝ
2		eqid 2085	. . 3 ⊢ 0 = 0
3	2	3mix1i 1113	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 8688	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 886	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 921   = wceq 1287   ∈ wcel 1436  ℝcr 7296  0cc0 7297  -cneg 7601  ℕcn 8360  ℤcz 8686

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-1re 7386  ax-addrcl 7389  ax-rnegex 7401

This theorem depends on definitions:  df-bi 115  df-3or 923  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-rab 2364  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-br 3823  df-iota 4948  df-fv 4991  df-ov 5618  df-neg 7603  df-z 8687

This theorem is referenced by:  0zd  8698  nn0ssz  8704  znegcl  8717  zgt0ge1  8744  nn0n0n1ge2b  8762  nn0lt10b  8763  nnm1ge0  8768  gtndiv  8777  msqznn  8782  zeo  8787  nn0ind  8796  fnn0ind  8798  nn0uz  8988  1eluzge0  8997  eqreznegel  9034  qreccl  9062  qdivcl  9063  irrmul  9067  fz10  9395  fz01en  9402  fzpreddisj  9418  fzshftral  9455  fznn0  9460  fz0tp  9466  elfz0ubfz0  9467  1fv  9481  lbfzo0  9523  elfzonlteqm1  9552  fzo01  9558  fzo0to2pr  9560  fzo0to3tp  9561  flqge0nn0  9631  divfl0  9634  btwnzge0  9638  modqmulnn  9680  zmodfz  9684  modqid  9687  zmodid2  9690  q0mod  9693  modqmuladdnn0  9706  frecfzennn  9764  expival  9877  qexpclz  9896  facdiv  10064  bcval  10075  bcnn  10083  bcm1k  10086  ibcval5  10089  bcpasc  10092  4bc2eq6  10100  hashinfom  10104  rexfiuz  10339  qabsor  10425  nn0abscl  10435  nnabscl  10450  climz  10596  climaddc1  10633  climmulc2  10635  climsubc1  10636  climsubc2  10637  climlec2  10645  dvdsval2  10724  dvdsdc  10729  moddvds  10730  dvds0  10736  0dvds  10741  zdvdsdc  10742  dvdscmulr  10750  dvdsmulcr  10751  dvdslelemd  10769  dvdsabseq  10773  divconjdvds  10775  alzdvds  10780  fzo0dvdseq  10783  odd2np1lem  10797  gcdmndc  10865  gcdsupex  10874  gcdsupcl  10875  gcd0val  10877  gcddvds  10880  gcd0id  10895  gcdid0  10896  gcdid  10902  bezoutlema  10913  bezoutlemb  10914  bezoutlembi  10919  dfgcd3  10924  dfgcd2  10928  gcdmultiplez  10935  dvdssq  10945  algcvgblem  10956  lcmmndc  10969  lcm0val  10972  dvdslcm  10976  lcmeq0  10978  lcmgcd  10985  lcmdvds  10986  lcmid  10987  3lcm2e6woprm  10993  6lcm4e12  10994  cncongr2  11011  sqrt2irrap  11083  dfphi2  11121  phiprmpw  11123  crth  11125  phimullem  11126  hashgcdeq  11129