Theorem 0z 9263

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 7956	. 2 ⊢ 0 ∈ ℝ
2		eqid 2177	. . 3 ⊢ 0 = 0
3	2	3mix1i 1169	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 9254	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 942	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 977   = wceq 1353   ∈ wcel 2148  ℝcr 7809  0cc0 7810  -cneg 8128  ℕcn 8918  ℤcz 9252

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1re 7904  ax-addrcl 7907  ax-rnegex 7919

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877  df-neg 8130  df-z 9253

This theorem is referenced by:  0zd  9264  nn0ssz  9270  znegcl  9283  zgt0ge1  9310  nn0n0n1ge2b  9331  nn0lt10b  9332  nnm1ge0  9338  gtndiv  9347  msqznn  9352  zeo  9357  nn0ind  9366  fnn0ind  9368  nn0uz  9561  1eluzge0  9573  elnn0dc  9610  eqreznegel  9613  qreccl  9641  qdivcl  9642  irrmul  9646  fz10  10045  fz01en  10052  fzpreddisj  10070  fzshftral  10107  fznn0  10112  fz1ssfz0  10116  fz0sn  10120  fz0tp  10121  fz0to3un2pr  10122  fz0to4untppr  10123  elfz0ubfz0  10124  1fv  10138  lbfzo0  10180  elfzonlteqm1  10209  fzo01  10215  fzo0to2pr  10217  fzo0to3tp  10218  flqge0nn0  10292  divfl0  10295  btwnzge0  10299  modqmulnn  10341  zmodfz  10345  modqid  10348  zmodid2  10351  q0mod  10354  modqmuladdnn0  10367  frecfzennn  10425  qexpclz  10540  qsqeqor  10630  facdiv  10717  bcval  10728  bcnn  10736  bcm1k  10739  bcval5  10742  bcpasc  10745  4bc2eq6  10753  hashinfom  10757  rexfiuz  10997  qabsor  11083  nn0abscl  11093  nnabscl  11108  climz  11299  climaddc1  11336  climmulc2  11338  climsubc1  11339  climsubc2  11340  climlec2  11348  binomlem  11490  binom  11491  bcxmas  11496  arisum2  11506  explecnv  11512  ef0lem  11667  dvdsval2  11796  dvdsdc  11804  moddvds  11805  dvds0  11812  0dvds  11817  zdvdsdc  11818  dvdscmulr  11826  dvdsmulcr  11827  dvdslelemd  11848  dvdsabseq  11852  divconjdvds  11854  alzdvds  11859  fzo0dvdseq  11862  odd2np1lem  11876  gcdmndc  11944  gcdsupex  11957  gcdsupcl  11958  gcd0val  11960  gcddvds  11963  gcd0id  11979  gcdid0  11980  gcdid  11986  bezoutlema  11999  bezoutlemb  12000  bezoutlembi  12005  dfgcd3  12010  dfgcd2  12014  gcdmultiplez  12021  dvdssq  12031  algcvgblem  12048  lcmmndc  12061  lcm0val  12064  dvdslcm  12068  lcmeq0  12070  lcmgcd  12077  lcmdvds  12078  lcmid  12079  3lcm2e6woprm  12085  6lcm4e12  12086  cncongr2  12103  sqrt2irrap  12179  dfphi2  12219  phiprmpw  12221  crth  12223  phimullem  12224  eulerthlemfi  12227  hashgcdeq  12238  phisum  12239  pceu  12294  pcdiv  12301  pc0  12303  pcqdiv  12306  pcexp  12308  pcxnn0cl  12309  pcxcl  12310  pcdvdstr  12325  dvdsprmpweqnn  12334  pcaddlem  12337  pcadd  12338  pcfaclem  12346  qexpz  12349  zgz  12370  igz  12371  ennnfonelemjn  12402  ennnfonelem1  12407  mulg0  12987  subgmulg  13046  zring0  13460  rpcxp0  14289  lgslem2  14372  lgsfcl2  14377  lgs0  14384  lgsneg  14395  lgsdilem  14398  lgsdir2lem3  14401  lgsdir  14406  lgsdilem2  14407  lgsdi  14408  lgsne0  14409  lgsprme0  14413  lgsdirnn0  14418  lgsdinn0  14419  apdifflemr  14765  apdiff  14766  iswomni0  14769  nconstwlpolem  14782