Theorem 0z 9198

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 7895	. 2 ⊢ 0 ∈ ℝ
2		eqid 2165	. . 3 ⊢ 0 = 0
3	2	3mix1i 1159	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 9189	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 932	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 967   = wceq 1343   ∈ wcel 2136  ℝcr 7748  0cc0 7749  -cneg 8066  ℕcn 8853  ℤcz 9187

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-1re 7843  ax-addrcl 7846  ax-rnegex 7858

This theorem depends on definitions:  df-bi 116  df-3or 969  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-ral 2448  df-rex 2449  df-rab 2452  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195  df-ov 5844  df-neg 8068  df-z 9188

This theorem is referenced by:  0zd  9199  nn0ssz  9205  znegcl  9218  zgt0ge1  9245  nn0n0n1ge2b  9266  nn0lt10b  9267  nnm1ge0  9273  gtndiv  9282  msqznn  9287  zeo  9292  nn0ind  9301  fnn0ind  9303  nn0uz  9496  1eluzge0  9508  elnn0dc  9545  eqreznegel  9548  qreccl  9576  qdivcl  9577  irrmul  9581  fz10  9977  fz01en  9984  fzpreddisj  10002  fzshftral  10039  fznn0  10044  fz1ssfz0  10048  fz0sn  10052  fz0tp  10053  fz0to3un2pr  10054  fz0to4untppr  10055  elfz0ubfz0  10056  1fv  10070  lbfzo0  10112  elfzonlteqm1  10141  fzo01  10147  fzo0to2pr  10149  fzo0to3tp  10150  flqge0nn0  10224  divfl0  10227  btwnzge0  10231  modqmulnn  10273  zmodfz  10277  modqid  10280  zmodid2  10283  q0mod  10286  modqmuladdnn0  10299  frecfzennn  10357  qexpclz  10472  qsqeqor  10561  facdiv  10647  bcval  10658  bcnn  10666  bcm1k  10669  bcval5  10672  bcpasc  10675  4bc2eq6  10683  hashinfom  10687  rexfiuz  10927  qabsor  11013  nn0abscl  11023  nnabscl  11038  climz  11229  climaddc1  11266  climmulc2  11268  climsubc1  11269  climsubc2  11270  climlec2  11278  binomlem  11420  binom  11421  bcxmas  11426  arisum2  11436  explecnv  11442  ef0lem  11597  dvdsval2  11726  dvdsdc  11734  moddvds  11735  dvds0  11742  0dvds  11747  zdvdsdc  11748  dvdscmulr  11756  dvdsmulcr  11757  dvdslelemd  11777  dvdsabseq  11781  divconjdvds  11783  alzdvds  11788  fzo0dvdseq  11791  odd2np1lem  11805  gcdmndc  11873  gcdsupex  11886  gcdsupcl  11887  gcd0val  11889  gcddvds  11892  gcd0id  11908  gcdid0  11909  gcdid  11915  bezoutlema  11928  bezoutlemb  11929  bezoutlembi  11934  dfgcd3  11939  dfgcd2  11943  gcdmultiplez  11950  dvdssq  11960  algcvgblem  11977  lcmmndc  11990  lcm0val  11993  dvdslcm  11997  lcmeq0  11999  lcmgcd  12006  lcmdvds  12007  lcmid  12008  3lcm2e6woprm  12014  6lcm4e12  12015  cncongr2  12032  sqrt2irrap  12108  dfphi2  12148  phiprmpw  12150  crth  12152  phimullem  12153  eulerthlemfi  12156  hashgcdeq  12167  phisum  12168  pceu  12223  pcdiv  12230  pc0  12232  pcqdiv  12235  pcexp  12237  pcxnn0cl  12238  pcxcl  12239  pcdvdstr  12254  dvdsprmpweqnn  12263  pcaddlem  12266  pcadd  12267  pcfaclem  12275  qexpz  12278  zgz  12299  igz  12300  ennnfonelemjn  12331  ennnfonelem1  12336  rpcxp0  13419  lgslem2  13502  lgsfcl2  13507  lgs0  13514  lgsneg  13525  lgsdilem  13528  lgsdir2lem3  13531  lgsdir  13536  lgsdilem2  13537  lgsdi  13538  lgsne0  13539  lgsprme0  13543  lgsdirnn0  13548  lgsdinn0  13549  apdifflemr  13886  apdiff  13887  iswomni0  13890  nconstwlpolem  13903