Theorem 0z 9480

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 8169	. 2 |- 0 e. RR
2		eqid 2229	. . 3 |- 0 = 0
3	2	3mix1i 1193	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9471	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 948	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 1001   = wceq 1395   e. wcel 2200   RRcr 8021   0cc0 8022   -ucneg 8341   NNcn 9133   ZZcz 9469

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8116  ax-addrcl 8119  ax-rnegex 8131

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016  df-neg 8343  df-z 9470

This theorem is referenced by:  0zd  9481  nn0ssz  9487  znegcl  9500  nnnle0  9518  zgt0ge1  9528  nn0n0n1ge2b  9549  nn0lt10b  9550  nnm1ge0  9556  gtndiv  9565  msqznn  9570  zeo  9575  nn0ind  9584  fnn0ind  9586  nn0uz  9781  1eluzge0  9798  elnn0dc  9835  eqreznegel  9838  qreccl  9866  qdivcl  9867  irrmul  9871  irrmulap  9872  fz10  10271  fz01en  10278  fzpreddisj  10296  fzshftral  10333  fznn0  10338  fz1ssfz0  10342  fz0sn  10346  fz0tp  10347  fz0to3un2pr  10348  fz0to4untppr  10349  elfz0ubfz0  10350  1fv  10364  fzo0n  10393  lbfzo0  10410  elfzonlteqm1  10445  fzo01  10451  fzo0to2pr  10453  fzo0to3tp  10454  flqge0nn0  10543  divfl0  10546  btwnzge0  10550  modqmulnn  10594  zmodfz  10598  modqid  10601  zmodid2  10604  q0mod  10607  modqmuladdnn0  10620  frecfzennn  10678  xnn0nnen  10689  qexpclz  10812  qsqeqor  10902  facdiv  10990  bcval  11001  bcnn  11009  bcm1k  11012  bcval5  11015  bcpasc  11018  4bc2eq6  11026  hashinfom  11030  iswrd  11105  iswrdiz  11110  wrdexg  11114  wrdfin  11122  wrdnval  11134  wrdred1hash  11147  lsw0  11151  ccatsymb  11169  ccatalpha  11180  s111  11198  ccat1st1st  11208  fzowrddc  11218  swrdlen  11223  swrdnd  11230  swrdwrdsymbg  11235  swrds1  11239  pfxval  11245  pfx00g  11246  pfx0g  11247  fnpfx  11248  pfxlen  11256  swrdccatin1  11296  swrdccat  11306  swrdccat3blem  11310  rexfiuz  11540  qabsor  11626  nn0abscl  11636  nnabscl  11651  climz  11843  climaddc1  11880  climmulc2  11882  climsubc1  11883  climsubc2  11884  climlec2  11892  binomlem  12034  binom  12035  bcxmas  12040  arisum2  12050  explecnv  12056  ef0lem  12211  dvdsval2  12341  dvdsdc  12349  moddvds  12350  dvds0  12357  0dvds  12362  zdvdsdc  12363  dvdscmulr  12371  dvdsmulcr  12372  fsumdvds  12393  dvdslelemd  12394  dvdsabseq  12398  divconjdvds  12400  alzdvds  12405  fzo0dvdseq  12408  odd2np1lem  12423  bitsfzo  12506  bitsmod  12507  0bits  12510  m1bits  12511  bitsinv1lem  12512  bitsinv1  12513  gcdmndc  12516  gcdsupex  12518  gcdsupcl  12519  gcd0val  12521  gcddvds  12524  gcd0id  12540  gcdid0  12541  gcdid  12547  bezoutlema  12560  bezoutlemb  12561  bezoutlembi  12566  dfgcd3  12571  dfgcd2  12575  gcdmultiplez  12582  dvdssq  12592  algcvgblem  12611  lcmmndc  12624  lcm0val  12627  dvdslcm  12631  lcmeq0  12633  lcmgcd  12640  lcmdvds  12641  lcmid  12642  3lcm2e6woprm  12648  6lcm4e12  12649  cncongr2  12666  sqrt2irrap  12742  dfphi2  12782  phiprmpw  12784  crth  12786  phimullem  12787  eulerthlemfi  12790  hashgcdeq  12802  phisum  12803  pceu  12858  pcdiv  12865  pc0  12867  pcqdiv  12870  pcexp  12872  pcxnn0cl  12873  pcxcl  12874  pcxqcl  12875  pcdvdstr  12890  dvdsprmpweqnn  12899  pcaddlem  12902  pcadd  12903  pcfaclem  12912  qexpz  12915  zgz  12936  igz  12937  4sqlem19  12972  ennnfonelemjn  13013  ennnfonelem1  13018  mulg0  13702  subgmulg  13765  zring0  14604  zndvds0  14654  znf1o  14655  znfi  14659  znhash  14660  psr1clfi  14692  plycolemc  15472  rpcxp0  15612  0sgm  15699  1sgmprm  15708  lgslem2  15720  lgsfcl2  15725  lgs0  15732  lgsneg  15743  lgsdilem  15746  lgsdir2lem3  15749  lgsdir  15754  lgsdilem2  15755  lgsdi  15756  lgsne0  15757  lgsprme0  15761  lgsdirnn0  15766  lgsdinn0  15767  usgrexmpldifpr  16088  wlkv0  16166  wlklenvclwlk  16170  upgr2wlkdc  16172  clwwlkccatlem  16195  eupthfi  16246  apdifflemr  16587  apdiff  16588  iswomni0  16591  nconstwlpolem  16605