Theorem 0z 9425

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 8114	. 2 ⊢ 0 ∈ ℝ
2		eqid 2209	. . 3 ⊢ 0 = 0
3	2	3mix1i 1174	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 9416	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 947	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 982   = wceq 1375   ∈ wcel 2180  ℝcr 7966  0cc0 7967  -cneg 8286  ℕcn 9078  ℤcz 9414

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191  ax-1re 8061  ax-addrcl 8064  ax-rnegex 8076

This theorem depends on definitions:  df-bi 117  df-3or 984  df-3an 985  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ral 2493  df-rex 2494  df-rab 2497  df-v 2781  df-un 3181  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-br 4063  df-iota 5254  df-fv 5302  df-ov 5977  df-neg 8288  df-z 9415

This theorem is referenced by:  0zd  9426  nn0ssz  9432  znegcl  9445  nnnle0  9463  zgt0ge1  9473  nn0n0n1ge2b  9494  nn0lt10b  9495  nnm1ge0  9501  gtndiv  9510  msqznn  9515  zeo  9520  nn0ind  9529  fnn0ind  9531  nn0uz  9725  1eluzge0  9737  elnn0dc  9774  eqreznegel  9777  qreccl  9805  qdivcl  9806  irrmul  9810  irrmulap  9811  fz10  10210  fz01en  10217  fzpreddisj  10235  fzshftral  10272  fznn0  10277  fz1ssfz0  10281  fz0sn  10285  fz0tp  10286  fz0to3un2pr  10287  fz0to4untppr  10288  elfz0ubfz0  10289  1fv  10303  fzo0n  10332  lbfzo0  10349  elfzonlteqm1  10383  fzo01  10389  fzo0to2pr  10391  fzo0to3tp  10392  flqge0nn0  10480  divfl0  10483  btwnzge0  10487  modqmulnn  10531  zmodfz  10535  modqid  10538  zmodid2  10541  q0mod  10544  modqmuladdnn0  10557  frecfzennn  10615  xnn0nnen  10626  qexpclz  10749  qsqeqor  10839  facdiv  10927  bcval  10938  bcnn  10946  bcm1k  10949  bcval5  10952  bcpasc  10955  4bc2eq6  10963  hashinfom  10967  iswrd  11040  iswrdiz  11045  wrdexg  11049  wrdfin  11057  wrdnval  11068  wrdred1hash  11081  lsw0  11085  ccatsymb  11103  s111  11130  ccat1st1st  11138  fzowrddc  11145  swrdlen  11150  swrdnd  11157  swrdwrdsymbg  11162  swrds1  11166  pfxval  11172  pfx00g  11173  pfx0g  11174  fnpfx  11175  pfxlen  11183  swrdccatin1  11223  swrdccat  11233  swrdccat3blem  11237  rexfiuz  11466  qabsor  11552  nn0abscl  11562  nnabscl  11577  climz  11769  climaddc1  11806  climmulc2  11808  climsubc1  11809  climsubc2  11810  climlec2  11818  binomlem  11960  binom  11961  bcxmas  11966  arisum2  11976  explecnv  11982  ef0lem  12137  dvdsval2  12267  dvdsdc  12275  moddvds  12276  dvds0  12283  0dvds  12288  zdvdsdc  12289  dvdscmulr  12297  dvdsmulcr  12298  fsumdvds  12319  dvdslelemd  12320  dvdsabseq  12324  divconjdvds  12326  alzdvds  12331  fzo0dvdseq  12334  odd2np1lem  12349  bitsfzo  12432  bitsmod  12433  0bits  12436  m1bits  12437  bitsinv1lem  12438  bitsinv1  12439  gcdmndc  12442  gcdsupex  12444  gcdsupcl  12445  gcd0val  12447  gcddvds  12450  gcd0id  12466  gcdid0  12467  gcdid  12473  bezoutlema  12486  bezoutlemb  12487  bezoutlembi  12492  dfgcd3  12497  dfgcd2  12501  gcdmultiplez  12508  dvdssq  12518  algcvgblem  12537  lcmmndc  12550  lcm0val  12553  dvdslcm  12557  lcmeq0  12559  lcmgcd  12566  lcmdvds  12567  lcmid  12568  3lcm2e6woprm  12574  6lcm4e12  12575  cncongr2  12592  sqrt2irrap  12668  dfphi2  12708  phiprmpw  12710  crth  12712  phimullem  12713  eulerthlemfi  12716  hashgcdeq  12728  phisum  12729  pceu  12784  pcdiv  12791  pc0  12793  pcqdiv  12796  pcexp  12798  pcxnn0cl  12799  pcxcl  12800  pcxqcl  12801  pcdvdstr  12816  dvdsprmpweqnn  12825  pcaddlem  12828  pcadd  12829  pcfaclem  12838  qexpz  12841  zgz  12862  igz  12863  4sqlem19  12898  ennnfonelemjn  12939  ennnfonelem1  12944  mulg0  13628  subgmulg  13691  zring0  14529  zndvds0  14579  znf1o  14580  znfi  14584  znhash  14585  psr1clfi  14617  plycolemc  15397  rpcxp0  15537  0sgm  15624  1sgmprm  15633  lgslem2  15645  lgsfcl2  15650  lgs0  15657  lgsneg  15668  lgsdilem  15671  lgsdir2lem3  15674  lgsdir  15679  lgsdilem2  15680  lgsdi  15681  lgsne0  15682  lgsprme0  15686  lgsdirnn0  15691  lgsdinn0  15692  apdifflemr  16326  apdiff  16327  iswomni0  16330  nconstwlpolem  16344