Theorem 0z 9337

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

Syntax hints:   ∨ w3o 979   = wceq 1364   ∈ wcel 2167  ℝcr 7878  0cc0 7879  -cneg 8198  ℕcn 8990  ℤcz 9326

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-1re 7973  ax-addrcl 7976  ax-rnegex 7988

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-rab 2484  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266  df-ov 5925  df-neg 8200  df-z 9327

This theorem is referenced by:  0zd  9338  nn0ssz  9344  znegcl  9357  zgt0ge1  9384  nn0n0n1ge2b  9405  nn0lt10b  9406  nnm1ge0  9412  gtndiv  9421  msqznn  9426  zeo  9431  nn0ind  9440  fnn0ind  9442  nn0uz  9636  1eluzge0  9648  elnn0dc  9685  eqreznegel  9688  qreccl  9716  qdivcl  9717  irrmul  9721  irrmulap  9722  fz10  10121  fz01en  10128  fzpreddisj  10146  fzshftral  10183  fznn0  10188  fz1ssfz0  10192  fz0sn  10196  fz0tp  10197  fz0to3un2pr  10198  fz0to4untppr  10199  elfz0ubfz0  10200  1fv  10214  lbfzo0  10257  elfzonlteqm1  10286  fzo01  10292  fzo0to2pr  10294  fzo0to3tp  10295  flqge0nn0  10383  divfl0  10386  btwnzge0  10390  modqmulnn  10434  zmodfz  10438  modqid  10441  zmodid2  10444  q0mod  10447  modqmuladdnn0  10460  frecfzennn  10518  xnn0nnen  10529  qexpclz  10652  qsqeqor  10742  facdiv  10830  bcval  10841  bcnn  10849  bcm1k  10852  bcval5  10855  bcpasc  10858  4bc2eq6  10866  hashinfom  10870  iswrd  10937  iswrdiz  10942  wrdexg  10946  wrdfin  10954  wrdnval  10965  wrdred1hash  10978  rexfiuz  11154  qabsor  11240  nn0abscl  11250  nnabscl  11265  climz  11457  climaddc1  11494  climmulc2  11496  climsubc1  11497  climsubc2  11498  climlec2  11506  binomlem  11648  binom  11649  bcxmas  11654  arisum2  11664  explecnv  11670  ef0lem  11825  dvdsval2  11955  dvdsdc  11963  moddvds  11964  dvds0  11971  0dvds  11976  zdvdsdc  11977  dvdscmulr  11985  dvdsmulcr  11986  fsumdvds  12007  dvdslelemd  12008  dvdsabseq  12012  divconjdvds  12014  alzdvds  12019  fzo0dvdseq  12022  odd2np1lem  12037  bitsfzo  12119  gcdmndc  12122  gcdsupex  12124  gcdsupcl  12125  gcd0val  12127  gcddvds  12130  gcd0id  12146  gcdid0  12147  gcdid  12153  bezoutlema  12166  bezoutlemb  12167  bezoutlembi  12172  dfgcd3  12177  dfgcd2  12181  gcdmultiplez  12188  dvdssq  12198  algcvgblem  12217  lcmmndc  12230  lcm0val  12233  dvdslcm  12237  lcmeq0  12239  lcmgcd  12246  lcmdvds  12247  lcmid  12248  3lcm2e6woprm  12254  6lcm4e12  12255  cncongr2  12272  sqrt2irrap  12348  dfphi2  12388  phiprmpw  12390  crth  12392  phimullem  12393  eulerthlemfi  12396  hashgcdeq  12408  phisum  12409  pceu  12464  pcdiv  12471  pc0  12473  pcqdiv  12476  pcexp  12478  pcxnn0cl  12479  pcxcl  12480  pcxqcl  12481  pcdvdstr  12496  dvdsprmpweqnn  12505  pcaddlem  12508  pcadd  12509  pcfaclem  12518  qexpz  12521  zgz  12542  igz  12543  4sqlem19  12578  ennnfonelemjn  12619  ennnfonelem1  12624  mulg0  13255  subgmulg  13318  zring0  14156  zndvds0  14206  znf1o  14207  znfi  14211  znhash  14212  plycolemc  14994  rpcxp0  15134  0sgm  15221  1sgmprm  15230  lgslem2  15242  lgsfcl2  15247  lgs0  15254  lgsneg  15265  lgsdilem  15268  lgsdir2lem3  15271  lgsdir  15276  lgsdilem2  15277  lgsdi  15278  lgsne0  15279  lgsprme0  15283  lgsdirnn0  15288  lgsdinn0  15289  apdifflemr  15691  apdiff  15692  iswomni0  15695  nconstwlpolem  15709