ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  0z GIF version

Theorem 0z 8312
Description: Zero is an integer. (Contributed by NM, 12-Jan-2002.)
Assertion
Ref Expression
0z 0 ∈ ℤ

Proof of Theorem 0z
StepHypRef Expression
1 0re 7084 . 2 0 ∈ ℝ
2 eqid 2056 . . 3 0 = 0
323mix1i 1087 . 2 (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4 elz 8303 . 2 (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
51, 3, 4mpbir2an 860 1 0 ∈ ℤ
Colors of variables: wff set class
Syntax hints:  w3o 895   = wceq 1259  wcel 1409  cr 6945  0cc0 6946  -cneg 7245  cn 7989  cz 8301
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-1re 7035  ax-addrcl 7038  ax-rnegex 7050
This theorem depends on definitions:  df-bi 114  df-3or 897  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-rab 2332  df-v 2576  df-un 2949  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-br 3792  df-iota 4894  df-fv 4937  df-ov 5542  df-neg 7247  df-z 8302
This theorem is referenced by:  0zd  8313  nn0ssz  8319  znegcl  8332  zgt0ge1  8359  nn0n0n1ge2b  8377  nn0lt10b  8378  nnm1ge0  8383  gtndiv  8392  msqznn  8396  zeo  8401  nn0ind  8410  fnn0ind  8412  nn0uz  8602  1eluzge0  8611  2eluzge0OLD  8613  eqreznegel  8645  qreccl  8673  qdivcl  8674  irrmul  8678  fz10  9011  fz01en  9018  fzpreddisj  9034  fzshftral  9071  fznn0  9075  fz0tp  9082  elfz0ubfz0  9083  1fv  9097  lbfzo0  9138  elfzonlteqm1  9167  fzo01  9173  fzo0to2pr  9175  fzo0to3tp  9176  flqge0nn0  9242  divfl0  9245  btwnzge0  9249  modqmulnn  9291  zmodfz  9295  modqid  9298  zmodid2  9301  q0mod  9304  modqmuladdnn0  9317  frecfzennn  9366  expival  9421  qexpclz  9440  facdiv  9605  bcval  9616  bcnn  9624  bcm1k  9627  ibcval5  9630  bcpasc  9633  4bc2eq6  9641  rexfiuz  9815  qabsor  9901  nn0abscl  9911  nnabscl  9926  climz  10043  climaddc1  10079  climmulc2  10081  climsubc1  10082  climsubc2  10083  climlec2  10091  dvdsval2  10110  dvdsdc  10115  moddvds  10116  dvds0  10122  0dvds  10127  dvdscmulr  10135  dvdsmulcr  10136  dvdslelemd  10154  dvdsabseq  10158  divconjdvds  10160  alzdvds  10165  fzo0dvdseq  10168  odd2np1lem  10182  algcvgblem  10257
  Copyright terms: Public domain W3C validator