Theorem 0z 9390

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 8079	. 2 ⊢ 0 ∈ ℝ
2		eqid 2206	. . 3 ⊢ 0 = 0
3	2	3mix1i 1172	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 9381	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 945	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 980   = wceq 1373   ∈ wcel 2177  ℝcr 7931  0cc0 7932  -cneg 8251  ℕcn 9043  ℤcz 9379

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-1re 8026  ax-addrcl 8029  ax-rnegex 8041

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-rab 2494  df-v 2775  df-un 3171  df-sn 3640  df-pr 3641  df-op 3643  df-uni 3853  df-br 4048  df-iota 5237  df-fv 5284  df-ov 5954  df-neg 8253  df-z 9380

This theorem is referenced by:  0zd  9391  nn0ssz  9397  znegcl  9410  nnnle0  9428  zgt0ge1  9438  nn0n0n1ge2b  9459  nn0lt10b  9460  nnm1ge0  9466  gtndiv  9475  msqznn  9480  zeo  9485  nn0ind  9494  fnn0ind  9496  nn0uz  9690  1eluzge0  9702  elnn0dc  9739  eqreznegel  9742  qreccl  9770  qdivcl  9771  irrmul  9775  irrmulap  9776  fz10  10175  fz01en  10182  fzpreddisj  10200  fzshftral  10237  fznn0  10242  fz1ssfz0  10246  fz0sn  10250  fz0tp  10251  fz0to3un2pr  10252  fz0to4untppr  10253  elfz0ubfz0  10254  1fv  10268  fzo0n  10297  lbfzo0  10312  elfzonlteqm1  10346  fzo01  10352  fzo0to2pr  10354  fzo0to3tp  10355  flqge0nn0  10443  divfl0  10446  btwnzge0  10450  modqmulnn  10494  zmodfz  10498  modqid  10501  zmodid2  10504  q0mod  10507  modqmuladdnn0  10520  frecfzennn  10578  xnn0nnen  10589  qexpclz  10712  qsqeqor  10802  facdiv  10890  bcval  10901  bcnn  10909  bcm1k  10912  bcval5  10915  bcpasc  10918  4bc2eq6  10926  hashinfom  10930  iswrd  11003  iswrdiz  11008  wrdexg  11012  wrdfin  11020  wrdnval  11031  wrdred1hash  11044  lsw0  11048  ccatsymb  11066  s111  11093  ccat1st1st  11101  fzowrddc  11108  swrdlen  11113  swrdnd  11120  swrdwrdsymbg  11125  swrds1  11129  pfxval  11135  pfx00g  11136  pfx0g  11137  pfxlen  11144  rexfiuz  11344  qabsor  11430  nn0abscl  11440  nnabscl  11455  climz  11647  climaddc1  11684  climmulc2  11686  climsubc1  11687  climsubc2  11688  climlec2  11696  binomlem  11838  binom  11839  bcxmas  11844  arisum2  11854  explecnv  11860  ef0lem  12015  dvdsval2  12145  dvdsdc  12153  moddvds  12154  dvds0  12161  0dvds  12166  zdvdsdc  12167  dvdscmulr  12175  dvdsmulcr  12176  fsumdvds  12197  dvdslelemd  12198  dvdsabseq  12202  divconjdvds  12204  alzdvds  12209  fzo0dvdseq  12212  odd2np1lem  12227  bitsfzo  12310  bitsmod  12311  0bits  12314  m1bits  12315  bitsinv1lem  12316  bitsinv1  12317  gcdmndc  12320  gcdsupex  12322  gcdsupcl  12323  gcd0val  12325  gcddvds  12328  gcd0id  12344  gcdid0  12345  gcdid  12351  bezoutlema  12364  bezoutlemb  12365  bezoutlembi  12370  dfgcd3  12375  dfgcd2  12379  gcdmultiplez  12386  dvdssq  12396  algcvgblem  12415  lcmmndc  12428  lcm0val  12431  dvdslcm  12435  lcmeq0  12437  lcmgcd  12444  lcmdvds  12445  lcmid  12446  3lcm2e6woprm  12452  6lcm4e12  12453  cncongr2  12470  sqrt2irrap  12546  dfphi2  12586  phiprmpw  12588  crth  12590  phimullem  12591  eulerthlemfi  12594  hashgcdeq  12606  phisum  12607  pceu  12662  pcdiv  12669  pc0  12671  pcqdiv  12674  pcexp  12676  pcxnn0cl  12677  pcxcl  12678  pcxqcl  12679  pcdvdstr  12694  dvdsprmpweqnn  12703  pcaddlem  12706  pcadd  12707  pcfaclem  12716  qexpz  12719  zgz  12740  igz  12741  4sqlem19  12776  ennnfonelemjn  12817  ennnfonelem1  12822  mulg0  13505  subgmulg  13568  zring0  14406  zndvds0  14456  znf1o  14457  znfi  14461  znhash  14462  psr1clfi  14494  plycolemc  15274  rpcxp0  15414  0sgm  15501  1sgmprm  15510  lgslem2  15522  lgsfcl2  15527  lgs0  15534  lgsneg  15545  lgsdilem  15548  lgsdir2lem3  15551  lgsdir  15556  lgsdilem2  15557  lgsdi  15558  lgsne0  15559  lgsprme0  15563  lgsdirnn0  15568  lgsdinn0  15569  apdifflemr  16060  apdiff  16061  iswomni0  16064  nconstwlpolem  16078