Theorem 0z 9634

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 8316	. 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 9625	. 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

Syntax hints:   \/ w3o 1008   = wceq 1402   e. wcel 2209   RRcr 8168   0cc0 8169   -ucneg 8488   NNcn 9283   ZZcz 9623

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 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 8263  ax-addrcl 8266  ax-rnegex 8278

This theorem 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 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380  df-ov 6078  df-neg 8490  df-z 9624

This theorem is referenced by:  0zd  9635  nn0ssz  9641  znegcl  9654  nnnle0  9672  zgt0ge1  9682  nn0n0n1ge2b  9704  nn0lt10b  9705  nnm1ge0  9711  gtndiv  9720  msqznn  9725  zeo  9730  nn0ind  9739  fnn0ind  9741  nn0uz  9936  1eluzge0  9953  elnn0dc  9990  eqreznegel  9993  qreccl  10021  qdivcl  10022  irrmul  10026  irrmulap  10027  fz10  10429  fz01en  10437  fzpreddisj  10456  fzshftral  10493  fznn0  10498  fz1ssfz0  10502  fz0sn  10506  fz0tp  10507  fz0to3un2pr  10508  fz0to4untppr  10509  elfz0ubfz0  10510  1fv  10524  fzo0n  10553  lbfzo0  10570  elfzonlteqm1  10606  fzo01  10612  fzo0to2pr  10614  fzo0to3tp  10615  flqge0nn0  10706  divfl0  10709  btwnzge0  10713  modqmulnn  10757  zmodfz  10761  modqid  10764  zmodid2  10767  q0mod  10770  modqmuladdnn0  10783  frecfzennn  10841  xnn0nnen  10852  qexpclz  10975  qsqeqor  11065  facdiv  11154  bcval  11165  bcnn  11173  bcm1k  11176  bcval5  11179  bcpasc  11182  4bc2eq6  11191  hashinfom  11195  hashfibc  11261  iswrd  11284  iswrdiz  11289  wrdexg  11293  wrdfin  11301  wrdnval  11313  wrdred1hash  11326  lsw0  11330  ccatsymb  11348  ccatalpha  11359  s111  11377  ccat1st1st  11387  fzowrddc  11397  swrdlen  11402  swrdnd  11409  swrdwrdsymbg  11414  swrds1  11418  pfxval  11424  pfx00g  11425  pfx0g  11426  fnpfx  11427  pfxlen  11435  swrdccatin1  11475  swrdccat  11485  swrdccat3blem  11489  rexfiuz  11733  qabsor  11819  nn0abscl  11829  nnabscl  11844  climz  12036  climaddc1  12073  climmulc2  12075  climsubc1  12076  climsubc2  12077  climlec2  12085  binomlem  12228  binom  12229  bcxmas  12234  arisum2  12244  explecnv  12250  ef0lem  12405  dvdsval2  12535  dvdsdc  12543  moddvds  12544  dvds0  12551  0dvds  12556  zdvdsdc  12557  dvdscmulr  12565  dvdsmulcr  12566  fsumdvds  12587  dvdslelemd  12588  dvdsabseq  12592  divconjdvds  12594  alzdvds  12599  fzo0dvdseq  12602  odd2np1lem  12617  bitsfzo  12700  bitsmod  12701  0bits  12704  m1bits  12705  bitsinv1lem  12706  bitsinv1  12707  gcdmndc  12710  gcdsupex  12712  gcdsupcl  12713  gcd0val  12715  gcddvds  12718  gcd0id  12734  gcdid0  12735  gcdid  12741  bezoutlema  12754  bezoutlemb  12755  bezoutlembi  12760  dfgcd3  12765  dfgcd2  12769  gcdmultiplez  12776  dvdssq  12786  algcvgblem  12805  lcmmndc  12818  lcm0val  12821  dvdslcm  12825  lcmeq0  12827  lcmgcd  12834  lcmdvds  12835  lcmid  12836  3lcm2e6woprm  12842  6lcm4e12  12843  cncongr2  12860  sqrt2irrap  12936  dfphi2  12976  phiprmpw  12978  crth  12980  phimullem  12981  eulerthlemfi  12984  hashgcdeq  12996  phisum  12997  pceu  13052  pcdiv  13059  pc0  13061  pcqdiv  13064  pcexp  13066  pcxnn0cl  13067  pcxcl  13068  pcxqcl  13069  pcdvdstr  13084  dvdsprmpweqnn  13093  pcaddlem  13096  pcadd  13097  pcfaclem  13106  qexpz  13109  zgz  13130  igz  13131  4sqlem19  13166  ballotfilemonn  13199  ballotfilem2  13206  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemefi  13215  ballotfilemodife  13218  ballotfilemscl  13225  ballotfilemsle  13226  ennnfonelemjn  13271  ennnfonelem1  13276  mulg0  13905  subgmulg  13968  zring0  14907  zndvds0  14957  znf1o  14958  znfi  14962  znhash  14963  psr1clfi  15002  plycolemc  15782  rpcxp0  15923  0sgm  16013  1sgmprm  16022  lgslem2  16034  lgsfcl2  16039  lgs0  16046  lgsneg  16057  lgsdilem  16060  lgsdir2lem3  16063  lgsdir  16068  lgsdilem2  16069  lgsdi  16070  lgsne0  16071  lgsprme0  16075  lgsdirnn0  16080  lgsdinn0  16081  usgrexmpldifpr  16404  vdegp1bid  16470  wlkv0  16524  wlklenvclwlk  16528  upgr2wlkdc  16532  clwwlkccatlem  16555  eupthfi  16606  trlsegvdeglem6  16620  konigsbergvtx  16637  konigsbergiedg  16638  konigsbergumgr  16642  konigsberglem1  16643  konigsberglem2  16644  konigsberglem3  16645  konigsberglem5  16647  konigsberg  16648  apdifflemr  17001  apdiff  17002  qdiff  17003  iswomni0  17006  nconstwlpolem  17020