Theorem 0z 9657

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 8326	. 2 ⊢ 0 ∈ ℝ
2		eqid 2238	. . 3 ⊢ 0 = 0
3	2	3mix1i 1200	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 9648	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 955	1 ⊢ 0 ∈ ℤ

This proof depends on syntax axioms:   ∨ w3o 1008   = wceq 1402   ∈ wcel 2209  ℝcr 8178  0cc0 8179  -cneg 8498  ℕcn 9305  ℤcz 9646

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1re 8273  ax-addrcl 8276  ax-rnegex 8288

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-rab 2537  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088  df-neg 8500  df-z 9647

This theorem is used by:  0zd  9658  nn0ssz  9664  znegcl  9677  nnnle0  9695  zgt0ge1  9705  nn0n0n1ge2b  9727  nn0lt10b  9728  nnm1ge0  9734  gtndiv  9743  msqznn  9748  zeo  9753  nn0ind  9762  fnn0ind  9764  nn0uz  9959  1eluzge0  9976  elnn0dc  10013  eqreznegel  10016  qreccl  10044  qdivcl  10045  irrmul  10049  irrmulap  10050  fz10  10452  fz00m1  10453  fz01en  10461  fzpreddisj  10480  fzshftral  10517  fznn0  10522  fz1ssfz0  10526  fz0sn  10530  fz0tp  10531  fz0to3un2pr  10532  fz0to4untppr  10533  elfz0ubfz0  10534  1fv  10548  fzo0n  10577  lbfzo0  10594  elfzonlteqm1  10630  fzo01  10636  fzo0to2pr  10638  fzo0to3tp  10639  flqge0nn0  10730  divfl0  10733  btwnzge0  10737  modqmulnn  10781  zmodfz  10785  modqid  10788  zmodid2  10791  q0mod  10794  modqmuladdnn0  10807  frecfzennn  10865  xnn0nnen  10876  qexpclz  10999  qsqeqor  11089  facdiv  11178  bcval  11189  bcnn  11197  bcm1k  11200  bcval5  11203  bcpasc  11206  4bc2eq6  11215  hashinfom  11219  hashfibc  11285  iswrd  11308  iswrdiz  11313  wrdexg  11317  wrdfin  11325  wrdnval  11337  wrdred1hash  11350  lsw0  11354  ccatsymb  11372  ccatalpha  11383  s111  11401  ccat1st1st  11411  fzowrddc  11421  swrdlen  11426  swrdnd  11433  swrdwrdsymbg  11438  swrds1  11442  pfxval  11448  pfx00g  11449  pfx0g  11450  fnpfx  11451  pfxlen  11459  swrdccatin1  11499  swrdccat  11509  swrdccat3blem  11513  rexfiuz  11757  qabsor  11843  nn0abscl  11853  nnabscl  11868  climz  12060  climaddc1  12097  climmulc2  12099  climsubc1  12100  climsubc2  12101  climlec2  12109  binomlem  12252  binom  12253  bcxmas  12258  arisum2  12268  explecnv  12274  ef0lem  12429  dvdsval2  12559  dvdsdc  12567  moddvds  12568  dvds0  12575  0dvds  12580  zdvdsdc  12581  dvdscmulr  12589  dvdsmulcr  12590  fsumdvds  12611  dvdslelemd  12612  dvdsabseq  12616  divconjdvds  12618  alzdvds  12623  fzo0dvdseq  12626  odd2np1lem  12641  bitsfzo  12724  bitsmod  12725  0bits  12728  m1bits  12729  bitsinv1lem  12730  bitsinv1  12731  gcdmndc  12734  gcdsupex  12736  gcdsupcl  12737  gcd0val  12739  gcddvds  12742  gcd0id  12758  gcdid0  12759  gcdid  12765  bezoutlema  12778  bezoutlemb  12779  bezoutlembi  12784  dfgcd3  12789  dfgcd2  12793  gcdmultiplez  12800  dvdssq  12810  algcvgblem  12829  lcmmndc  12842  lcm0val  12845  dvdslcm  12849  lcmeq0  12851  lcmgcd  12858  lcmdvds  12859  lcmid  12860  3lcm2e6woprm  12866  6lcm4e12  12867  cncongr2  12884  sqrt2irrap  12960  dfphi2  13000  phiprmpw  13002  crth  13004  phimullem  13005  eulerthlemfi  13008  hashgcdeq  13020  phisum  13021  pceu  13076  pcdiv  13083  pc0  13085  pcqdiv  13088  pcexp  13090  pcxnn0cl  13091  pcxcl  13092  pcxqcl  13093  pcdvdstr  13108  dvdsprmpweqnn  13117  pcaddlem  13120  pcadd  13121  pcfaclem  13130  qexpz  13133  zgz  13154  igz  13155  4sqlem19  13190  ballotfilemonn  13223  ballotfilem2  13230  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemefi  13239  ballotfilemodife  13242  ballotfilemscl  13249  ballotfilemsle  13250  ennnfonelemjn  13295  ennnfonelem1  13300  mulg0  13930  subgmulg  13993  zring0  14937  zndvds0  14987  znf1o  14988  znfi  14992  znhash  14993  psr1clfi  15081  plycolemc  15861  rpcxp0  16006  0sgm  16105  1sgmprm  16114  bcmono  16124  lgslem2  16132  lgsfcl2  16137  lgs0  16144  lgsneg  16155  lgsdilem  16158  lgsdir2lem3  16161  lgsdir  16166  lgsdilem2  16167  lgsdi  16168  lgsne0  16169  lgsprme0  16173  lgsdirnn0  16178  lgsdinn0  16179  usgrexmpldifpr  16502  vdegp1bid  16568  wlkv0  16622  wlklenvclwlk  16626  upgr2wlkdc  16630  clwwlkccatlem  16653  eupthfi  16704  trlsegvdeglem6  16718  konigsbergvtx  16735  konigsbergiedg  16736  konigsbergumgr  16740  konigsberglem1  16741  konigsberglem2  16742  konigsberglem3  16743  konigsberglem5  16745  konigsberg  16746  apdifflemr  17108  apdiff  17109  qdiff  17110  iswomni0  17113  nconstwlpolem  17127