Theorem 0z 9328

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

Syntax hints:   ∨ w3o 979   = wceq 1364   ∈ wcel 2164  ℝcr 7871  0cc0 7872  -cneg 8191  ℕcn 8982  ℤcz 9317

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 2175  ax-1re 7966  ax-addrcl 7969  ax-rnegex 7981

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 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-rab 2481  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262  df-ov 5921  df-neg 8193  df-z 9318

This theorem is referenced by:  0zd  9329  nn0ssz  9335  znegcl  9348  zgt0ge1  9375  nn0n0n1ge2b  9396  nn0lt10b  9397  nnm1ge0  9403  gtndiv  9412  msqznn  9417  zeo  9422  nn0ind  9431  fnn0ind  9433  nn0uz  9627  1eluzge0  9639  elnn0dc  9676  eqreznegel  9679  qreccl  9707  qdivcl  9708  irrmul  9712  irrmulap  9713  fz10  10112  fz01en  10119  fzpreddisj  10137  fzshftral  10174  fznn0  10179  fz1ssfz0  10183  fz0sn  10187  fz0tp  10188  fz0to3un2pr  10189  fz0to4untppr  10190  elfz0ubfz0  10191  1fv  10205  lbfzo0  10248  elfzonlteqm1  10277  fzo01  10283  fzo0to2pr  10285  fzo0to3tp  10286  flqge0nn0  10362  divfl0  10365  btwnzge0  10369  modqmulnn  10413  zmodfz  10417  modqid  10420  zmodid2  10423  q0mod  10426  modqmuladdnn0  10439  frecfzennn  10497  xnn0nnen  10508  qexpclz  10631  qsqeqor  10721  facdiv  10809  bcval  10820  bcnn  10828  bcm1k  10831  bcval5  10834  bcpasc  10837  4bc2eq6  10845  hashinfom  10849  iswrd  10916  iswrdiz  10921  wrdexg  10925  wrdfin  10933  wrdnval  10944  wrdred1hash  10957  rexfiuz  11133  qabsor  11219  nn0abscl  11229  nnabscl  11244  climz  11435  climaddc1  11472  climmulc2  11474  climsubc1  11475  climsubc2  11476  climlec2  11484  binomlem  11626  binom  11627  bcxmas  11632  arisum2  11642  explecnv  11648  ef0lem  11803  dvdsval2  11933  dvdsdc  11941  moddvds  11942  dvds0  11949  0dvds  11954  zdvdsdc  11955  dvdscmulr  11963  dvdsmulcr  11964  dvdslelemd  11985  dvdsabseq  11989  divconjdvds  11991  alzdvds  11996  fzo0dvdseq  11999  odd2np1lem  12013  gcdmndc  12081  gcdsupex  12094  gcdsupcl  12095  gcd0val  12097  gcddvds  12100  gcd0id  12116  gcdid0  12117  gcdid  12123  bezoutlema  12136  bezoutlemb  12137  bezoutlembi  12142  dfgcd3  12147  dfgcd2  12151  gcdmultiplez  12158  dvdssq  12168  algcvgblem  12187  lcmmndc  12200  lcm0val  12203  dvdslcm  12207  lcmeq0  12209  lcmgcd  12216  lcmdvds  12217  lcmid  12218  3lcm2e6woprm  12224  6lcm4e12  12225  cncongr2  12242  sqrt2irrap  12318  dfphi2  12358  phiprmpw  12360  crth  12362  phimullem  12363  eulerthlemfi  12366  hashgcdeq  12377  phisum  12378  pceu  12433  pcdiv  12440  pc0  12442  pcqdiv  12445  pcexp  12447  pcxnn0cl  12448  pcxcl  12449  pcxqcl  12450  pcdvdstr  12465  dvdsprmpweqnn  12474  pcaddlem  12477  pcadd  12478  pcfaclem  12487  qexpz  12490  zgz  12511  igz  12512  4sqlem19  12547  ennnfonelemjn  12559  ennnfonelem1  12564  mulg0  13195  subgmulg  13258  zring0  14088  zndvds0  14138  znf1o  14139  znfi  14143  znhash  14144  rpcxp0  15033  lgslem2  15117  lgsfcl2  15122  lgs0  15129  lgsneg  15140  lgsdilem  15143  lgsdir2lem3  15146  lgsdir  15151  lgsdilem2  15152  lgsdi  15153  lgsne0  15154  lgsprme0  15158  lgsdirnn0  15163  lgsdinn0  15164  apdifflemr  15537  apdiff  15538  iswomni0  15541  nconstwlpolem  15555