Theorem 0z 9655

Description: Zero is an integer. (Contributed by NM, 12-Jan-2002.)

Assertion

Ref	Expression
0z	|- 0 e. ZZ

Proof of Theorem 0z

Step	Hyp	Ref	Expression
1		0re 8326	. 2 |- 0 e. RR
2		eqid 2238	. . 3 |- 0 = 0
3	2	3mix1i 1200	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9646	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 955	1 |- 0 e. ZZ

This proof depends on syntax axioms:   \/ w3o 1008   = wceq 1402   e. wcel 2209   RRcr 8178   0cc0 8179   -ucneg 8498   NNcn 9304   ZZcz 9644

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 9645

This theorem is used by:  0zd  9656  nn0ssz  9662  znegcl  9675  nnnle0  9693  zgt0ge1  9703  nn0n0n1ge2b  9725  nn0lt10b  9726  nnm1ge0  9732  gtndiv  9741  msqznn  9746  zeo  9751  nn0ind  9760  fnn0ind  9762  nn0uz  9957  1eluzge0  9974  elnn0dc  10011  eqreznegel  10014  qreccl  10042  qdivcl  10043  irrmul  10047  irrmulap  10048  fz10  10450  fz00m1  10451  fz01en  10459  fzpreddisj  10478  fzshftral  10515  fznn0  10520  fz1ssfz0  10524  fz0sn  10528  fz0tp  10529  fz0to3un2pr  10530  fz0to4untppr  10531  elfz0ubfz0  10532  1fv  10546  fzo0n  10575  lbfzo0  10592  elfzonlteqm1  10628  fzo01  10634  fzo0to2pr  10636  fzo0to3tp  10637  flqge0nn0  10728  divfl0  10731  btwnzge0  10735  modqmulnn  10779  zmodfz  10783  modqid  10786  zmodid2  10789  q0mod  10792  modqmuladdnn0  10805  frecfzennn  10863  xnn0nnen  10874  qexpclz  10997  qsqeqor  11087  facdiv  11176  bcval  11187  bcnn  11195  bcm1k  11198  bcval5  11201  bcpasc  11204  4bc2eq6  11213  hashinfom  11217  hashfibc  11283  iswrd  11306  iswrdiz  11311  wrdexg  11315  wrdfin  11323  wrdnval  11335  wrdred1hash  11348  lsw0  11352  ccatsymb  11370  ccatalpha  11381  s111  11399  ccat1st1st  11409  fzowrddc  11419  swrdlen  11424  swrdnd  11431  swrdwrdsymbg  11436  swrds1  11440  pfxval  11446  pfx00g  11447  pfx0g  11448  fnpfx  11449  pfxlen  11457  swrdccatin1  11497  swrdccat  11507  swrdccat3blem  11511  rexfiuz  11755  qabsor  11841  nn0abscl  11851  nnabscl  11866  climz  12058  climaddc1  12095  climmulc2  12097  climsubc1  12098  climsubc2  12099  climlec2  12107  binomlem  12250  binom  12251  bcxmas  12256  arisum2  12266  explecnv  12272  ef0lem  12427  dvdsval2  12557  dvdsdc  12565  moddvds  12566  dvds0  12573  0dvds  12578  zdvdsdc  12579  dvdscmulr  12587  dvdsmulcr  12588  fsumdvds  12609  dvdslelemd  12610  dvdsabseq  12614  divconjdvds  12616  alzdvds  12621  fzo0dvdseq  12624  odd2np1lem  12639  bitsfzo  12722  bitsmod  12723  0bits  12726  m1bits  12727  bitsinv1lem  12728  bitsinv1  12729  gcdmndc  12732  gcdsupex  12734  gcdsupcl  12735  gcd0val  12737  gcddvds  12740  gcd0id  12756  gcdid0  12757  gcdid  12763  bezoutlema  12776  bezoutlemb  12777  bezoutlembi  12782  dfgcd3  12787  dfgcd2  12791  gcdmultiplez  12798  dvdssq  12808  algcvgblem  12827  lcmmndc  12840  lcm0val  12843  dvdslcm  12847  lcmeq0  12849  lcmgcd  12856  lcmdvds  12857  lcmid  12858  3lcm2e6woprm  12864  6lcm4e12  12865  cncongr2  12882  sqrt2irrap  12958  dfphi2  12998  phiprmpw  13000  crth  13002  phimullem  13003  eulerthlemfi  13006  hashgcdeq  13018  phisum  13019  pceu  13074  pcdiv  13081  pc0  13083  pcqdiv  13086  pcexp  13088  pcxnn0cl  13089  pcxcl  13090  pcxqcl  13091  pcdvdstr  13106  dvdsprmpweqnn  13115  pcaddlem  13118  pcadd  13119  pcfaclem  13128  qexpz  13131  zgz  13152  igz  13153  4sqlem19  13188  ballotfilemonn  13221  ballotfilem2  13228  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemefi  13237  ballotfilemodife  13240  ballotfilemscl  13247  ballotfilemsle  13248  ennnfonelemjn  13293  ennnfonelem1  13298  mulg0  13928  subgmulg  13991  zring0  14935  zndvds0  14985  znf1o  14986  znfi  14990  znhash  14991  psr1clfi  15079  plycolemc  15859  rpcxp0  16000  0sgm  16099  1sgmprm  16108  lgslem2  16120  lgsfcl2  16125  lgs0  16132  lgsneg  16143  lgsdilem  16146  lgsdir2lem3  16149  lgsdir  16154  lgsdilem2  16155  lgsdi  16156  lgsne0  16157  lgsprme0  16161  lgsdirnn0  16166  lgsdinn0  16167  usgrexmpldifpr  16490  vdegp1bid  16556  wlkv0  16610  wlklenvclwlk  16614  upgr2wlkdc  16618  clwwlkccatlem  16641  eupthfi  16692  trlsegvdeglem6  16706  konigsbergvtx  16723  konigsbergiedg  16724  konigsbergumgr  16728  konigsberglem1  16729  konigsberglem2  16730  konigsberglem3  16731  konigsberglem5  16733  konigsberg  16734  apdifflemr  17096  apdiff  17097  qdiff  17098  iswomni0  17101  nconstwlpolem  17115