Theorem 0z 9605

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 8290	. 2 |- 0 e. RR
2		eqid 2234	. . 3 |- 0 = 0
3	2	3mix1i 1196	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9596	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 951	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 1004   = wceq 1398   e. wcel 2205   RRcr 8142   0cc0 8143   -ucneg 8461   NNcn 9254   ZZcz 9594

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-1re 8237  ax-addrcl 8240  ax-rnegex 8252

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-rab 2531  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061  df-neg 8463  df-z 9595

This theorem is referenced by:  0zd  9606  nn0ssz  9612  znegcl  9625  nnnle0  9643  zgt0ge1  9653  nn0n0n1ge2b  9675  nn0lt10b  9676  nnm1ge0  9682  gtndiv  9691  msqznn  9696  zeo  9701  nn0ind  9710  fnn0ind  9712  nn0uz  9907  1eluzge0  9924  elnn0dc  9961  eqreznegel  9964  qreccl  9992  qdivcl  9993  irrmul  9997  irrmulap  9998  fz10  10400  fz01en  10408  fzpreddisj  10427  fzshftral  10464  fznn0  10469  fz1ssfz0  10473  fz0sn  10477  fz0tp  10478  fz0to3un2pr  10479  fz0to4untppr  10480  elfz0ubfz0  10481  1fv  10495  fzo0n  10524  lbfzo0  10541  elfzonlteqm1  10577  fzo01  10583  fzo0to2pr  10585  fzo0to3tp  10586  flqge0nn0  10677  divfl0  10680  btwnzge0  10684  modqmulnn  10728  zmodfz  10732  modqid  10735  zmodid2  10738  q0mod  10741  modqmuladdnn0  10754  frecfzennn  10812  xnn0nnen  10823  qexpclz  10946  qsqeqor  11036  facdiv  11125  bcval  11136  bcnn  11144  bcm1k  11147  bcval5  11150  bcpasc  11153  4bc2eq6  11162  hashinfom  11166  hashfibc  11232  iswrd  11251  iswrdiz  11256  wrdexg  11260  wrdfin  11268  wrdnval  11280  wrdred1hash  11293  lsw0  11297  ccatsymb  11315  ccatalpha  11326  s111  11344  ccat1st1st  11354  fzowrddc  11364  swrdlen  11369  swrdnd  11376  swrdwrdsymbg  11381  swrds1  11385  pfxval  11391  pfx00g  11392  pfx0g  11393  fnpfx  11394  pfxlen  11402  swrdccatin1  11442  swrdccat  11452  swrdccat3blem  11456  rexfiuz  11699  qabsor  11785  nn0abscl  11795  nnabscl  11810  climz  12002  climaddc1  12039  climmulc2  12041  climsubc1  12042  climsubc2  12043  climlec2  12051  binomlem  12194  binom  12195  bcxmas  12200  arisum2  12210  explecnv  12216  ef0lem  12371  dvdsval2  12501  dvdsdc  12509  moddvds  12510  dvds0  12517  0dvds  12522  zdvdsdc  12523  dvdscmulr  12531  dvdsmulcr  12532  fsumdvds  12553  dvdslelemd  12554  dvdsabseq  12558  divconjdvds  12560  alzdvds  12565  fzo0dvdseq  12568  odd2np1lem  12583  bitsfzo  12666  bitsmod  12667  0bits  12670  m1bits  12671  bitsinv1lem  12672  bitsinv1  12673  gcdmndc  12676  gcdsupex  12678  gcdsupcl  12679  gcd0val  12681  gcddvds  12684  gcd0id  12700  gcdid0  12701  gcdid  12707  bezoutlema  12720  bezoutlemb  12721  bezoutlembi  12726  dfgcd3  12731  dfgcd2  12735  gcdmultiplez  12742  dvdssq  12752  algcvgblem  12771  lcmmndc  12784  lcm0val  12787  dvdslcm  12791  lcmeq0  12793  lcmgcd  12800  lcmdvds  12801  lcmid  12802  3lcm2e6woprm  12808  6lcm4e12  12809  cncongr2  12826  sqrt2irrap  12902  dfphi2  12942  phiprmpw  12944  crth  12946  phimullem  12947  eulerthlemfi  12950  hashgcdeq  12962  phisum  12963  pceu  13018  pcdiv  13025  pc0  13027  pcqdiv  13030  pcexp  13032  pcxnn0cl  13033  pcxcl  13034  pcxqcl  13035  pcdvdstr  13050  dvdsprmpweqnn  13059  pcaddlem  13062  pcadd  13063  pcfaclem  13072  qexpz  13075  zgz  13096  igz  13097  4sqlem19  13132  ballotfilemonn  13165  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemefi  13181  ballotfilemodife  13184  ballotfilemscl  13191  ballotfilemsle  13192  ennnfonelemjn  13237  ennnfonelem1  13242  mulg0  13878  subgmulg  13941  zring0  14874  zndvds0  14924  znf1o  14925  znfi  14929  znhash  14930  psr1clfi  14969  plycolemc  15749  rpcxp0  15889  0sgm  15979  1sgmprm  15988  lgslem2  16000  lgsfcl2  16005  lgs0  16012  lgsneg  16023  lgsdilem  16026  lgsdir2lem3  16029  lgsdir  16034  lgsdilem2  16035  lgsdi  16036  lgsne0  16037  lgsprme0  16041  lgsdirnn0  16046  lgsdinn0  16047  usgrexmpldifpr  16370  vdegp1bid  16436  wlkv0  16490  wlklenvclwlk  16494  upgr2wlkdc  16498  clwwlkccatlem  16521  eupthfi  16572  trlsegvdeglem6  16586  konigsbergvtx  16603  konigsbergiedg  16604  konigsbergumgr  16608  konigsberglem1  16609  konigsberglem2  16610  konigsberglem3  16611  konigsberglem5  16613  konigsberg  16614  apdifflemr  16957  apdiff  16958  qdiff  16959  iswomni0  16962  nconstwlpolem  16977