Theorem 0z 9489

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 8178	. 2 |- 0 e. RR
2		eqid 2231	. . 3 |- 0 = 0
3	2	3mix1i 1195	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9480	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 950	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 1003   = wceq 1397   e. wcel 2202   RRcr 8030   0cc0 8031   -ucneg 8350   NNcn 9142   ZZcz 9478

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1re 8125  ax-addrcl 8128  ax-rnegex 8140

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6020  df-neg 8352  df-z 9479

This theorem is referenced by:  0zd  9490  nn0ssz  9496  znegcl  9509  nnnle0  9527  zgt0ge1  9537  nn0n0n1ge2b  9558  nn0lt10b  9559  nnm1ge0  9565  gtndiv  9574  msqznn  9579  zeo  9584  nn0ind  9593  fnn0ind  9595  nn0uz  9790  1eluzge0  9807  elnn0dc  9844  eqreznegel  9847  qreccl  9875  qdivcl  9876  irrmul  9880  irrmulap  9881  fz10  10280  fz01en  10287  fzpreddisj  10305  fzshftral  10342  fznn0  10347  fz1ssfz0  10351  fz0sn  10355  fz0tp  10356  fz0to3un2pr  10357  fz0to4untppr  10358  elfz0ubfz0  10359  1fv  10373  fzo0n  10402  lbfzo0  10419  elfzonlteqm1  10454  fzo01  10460  fzo0to2pr  10462  fzo0to3tp  10463  flqge0nn0  10552  divfl0  10555  btwnzge0  10559  modqmulnn  10603  zmodfz  10607  modqid  10610  zmodid2  10613  q0mod  10616  modqmuladdnn0  10629  frecfzennn  10687  xnn0nnen  10698  qexpclz  10821  qsqeqor  10911  facdiv  10999  bcval  11010  bcnn  11018  bcm1k  11021  bcval5  11024  bcpasc  11027  4bc2eq6  11035  hashinfom  11039  iswrd  11114  iswrdiz  11119  wrdexg  11123  wrdfin  11131  wrdnval  11143  wrdred1hash  11156  lsw0  11160  ccatsymb  11178  ccatalpha  11189  s111  11207  ccat1st1st  11217  fzowrddc  11227  swrdlen  11232  swrdnd  11239  swrdwrdsymbg  11244  swrds1  11248  pfxval  11254  pfx00g  11255  pfx0g  11256  fnpfx  11257  pfxlen  11265  swrdccatin1  11305  swrdccat  11315  swrdccat3blem  11319  rexfiuz  11549  qabsor  11635  nn0abscl  11645  nnabscl  11660  climz  11852  climaddc1  11889  climmulc2  11891  climsubc1  11892  climsubc2  11893  climlec2  11901  binomlem  12043  binom  12044  bcxmas  12049  arisum2  12059  explecnv  12065  ef0lem  12220  dvdsval2  12350  dvdsdc  12358  moddvds  12359  dvds0  12366  0dvds  12371  zdvdsdc  12372  dvdscmulr  12380  dvdsmulcr  12381  fsumdvds  12402  dvdslelemd  12403  dvdsabseq  12407  divconjdvds  12409  alzdvds  12414  fzo0dvdseq  12417  odd2np1lem  12432  bitsfzo  12515  bitsmod  12516  0bits  12519  m1bits  12520  bitsinv1lem  12521  bitsinv1  12522  gcdmndc  12525  gcdsupex  12527  gcdsupcl  12528  gcd0val  12530  gcddvds  12533  gcd0id  12549  gcdid0  12550  gcdid  12556  bezoutlema  12569  bezoutlemb  12570  bezoutlembi  12575  dfgcd3  12580  dfgcd2  12584  gcdmultiplez  12591  dvdssq  12601  algcvgblem  12620  lcmmndc  12633  lcm0val  12636  dvdslcm  12640  lcmeq0  12642  lcmgcd  12649  lcmdvds  12650  lcmid  12651  3lcm2e6woprm  12657  6lcm4e12  12658  cncongr2  12675  sqrt2irrap  12751  dfphi2  12791  phiprmpw  12793  crth  12795  phimullem  12796  eulerthlemfi  12799  hashgcdeq  12811  phisum  12812  pceu  12867  pcdiv  12874  pc0  12876  pcqdiv  12879  pcexp  12881  pcxnn0cl  12882  pcxcl  12883  pcxqcl  12884  pcdvdstr  12899  dvdsprmpweqnn  12908  pcaddlem  12911  pcadd  12912  pcfaclem  12921  qexpz  12924  zgz  12945  igz  12946  4sqlem19  12981  ennnfonelemjn  13022  ennnfonelem1  13027  mulg0  13711  subgmulg  13774  zring0  14613  zndvds0  14663  znf1o  14664  znfi  14668  znhash  14669  psr1clfi  14701  plycolemc  15481  rpcxp0  15621  0sgm  15708  1sgmprm  15717  lgslem2  15729  lgsfcl2  15734  lgs0  15741  lgsneg  15752  lgsdilem  15755  lgsdir2lem3  15758  lgsdir  15763  lgsdilem2  15764  lgsdi  15765  lgsne0  15766  lgsprme0  15770  lgsdirnn0  15775  lgsdinn0  15776  usgrexmpldifpr  16099  vdegp1bid  16165  wlkv0  16219  wlklenvclwlk  16223  upgr2wlkdc  16227  clwwlkccatlem  16250  eupthfi  16301  trlsegvdeglem6  16315  apdifflemr  16651  apdiff  16652  iswomni0  16655  nconstwlpolem  16669