Theorem 0z 9294

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 7987	. 2 ⊢ 0 ∈ ℝ
2		eqid 2189	. . 3 ⊢ 0 = 0
3	2	3mix1i 1171	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 9285	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 944	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 979   = wceq 1364   ∈ wcel 2160  ℝcr 7840  0cc0 7841  -cneg 8159  ℕcn 8949  ℤcz 9283

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-1re 7935  ax-addrcl 7938  ax-rnegex 7950

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-rab 2477  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-iota 5196  df-fv 5243  df-ov 5899  df-neg 8161  df-z 9284

This theorem is referenced by:  0zd  9295  nn0ssz  9301  znegcl  9314  zgt0ge1  9341  nn0n0n1ge2b  9362  nn0lt10b  9363  nnm1ge0  9369  gtndiv  9378  msqznn  9383  zeo  9388  nn0ind  9397  fnn0ind  9399  nn0uz  9592  1eluzge0  9604  elnn0dc  9641  eqreznegel  9644  qreccl  9672  qdivcl  9673  irrmul  9677  fz10  10076  fz01en  10083  fzpreddisj  10101  fzshftral  10138  fznn0  10143  fz1ssfz0  10147  fz0sn  10151  fz0tp  10152  fz0to3un2pr  10153  fz0to4untppr  10154  elfz0ubfz0  10155  1fv  10169  lbfzo0  10211  elfzonlteqm1  10240  fzo01  10246  fzo0to2pr  10248  fzo0to3tp  10249  flqge0nn0  10324  divfl0  10327  btwnzge0  10331  modqmulnn  10373  zmodfz  10377  modqid  10380  zmodid2  10383  q0mod  10386  modqmuladdnn0  10399  frecfzennn  10457  qexpclz  10572  qsqeqor  10662  facdiv  10750  bcval  10761  bcnn  10769  bcm1k  10772  bcval5  10775  bcpasc  10778  4bc2eq6  10786  hashinfom  10790  rexfiuz  11030  qabsor  11116  nn0abscl  11126  nnabscl  11141  climz  11332  climaddc1  11369  climmulc2  11371  climsubc1  11372  climsubc2  11373  climlec2  11381  binomlem  11523  binom  11524  bcxmas  11529  arisum2  11539  explecnv  11545  ef0lem  11700  dvdsval2  11829  dvdsdc  11837  moddvds  11838  dvds0  11845  0dvds  11850  zdvdsdc  11851  dvdscmulr  11859  dvdsmulcr  11860  dvdslelemd  11881  dvdsabseq  11885  divconjdvds  11887  alzdvds  11892  fzo0dvdseq  11895  odd2np1lem  11909  gcdmndc  11977  gcdsupex  11990  gcdsupcl  11991  gcd0val  11993  gcddvds  11996  gcd0id  12012  gcdid0  12013  gcdid  12019  bezoutlema  12032  bezoutlemb  12033  bezoutlembi  12038  dfgcd3  12043  dfgcd2  12047  gcdmultiplez  12054  dvdssq  12064  algcvgblem  12081  lcmmndc  12094  lcm0val  12097  dvdslcm  12101  lcmeq0  12103  lcmgcd  12110  lcmdvds  12111  lcmid  12112  3lcm2e6woprm  12118  6lcm4e12  12119  cncongr2  12136  sqrt2irrap  12212  dfphi2  12252  phiprmpw  12254  crth  12256  phimullem  12257  eulerthlemfi  12260  hashgcdeq  12271  phisum  12272  pceu  12327  pcdiv  12334  pc0  12336  pcqdiv  12339  pcexp  12341  pcxnn0cl  12342  pcxcl  12343  pcxqcl  12344  pcdvdstr  12359  dvdsprmpweqnn  12368  pcaddlem  12371  pcadd  12372  pcfaclem  12381  qexpz  12384  zgz  12405  igz  12406  4sqlem19  12441  ennnfonelemjn  12453  ennnfonelem1  12458  mulg0  13067  subgmulg  13127  zring0  13899  rpcxp0  14776  lgslem2  14860  lgsfcl2  14865  lgs0  14872  lgsneg  14883  lgsdilem  14886  lgsdir2lem3  14889  lgsdir  14894  lgsdilem2  14895  lgsdi  14896  lgsne0  14897  lgsprme0  14901  lgsdirnn0  14906  lgsdinn0  14907  apdifflemr  15254  apdiff  15255  iswomni0  15258  nconstwlpolem  15272