Theorem 0z 9295

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 7988	. 2 |- 0 e. RR
2		eqid 2189	. . 3 |- 0 = 0
3	2	3mix1i 1171	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9286	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 944	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 979   = wceq 1364   e. wcel 2160   RRcr 7841   0cc0 7842   -ucneg 8160   NNcn 8950   ZZcz 9284

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-1re 7936  ax-addrcl 7939  ax-rnegex 7951

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-rab 2477  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-iota 5196  df-fv 5243  df-ov 5900  df-neg 8162  df-z 9285

This theorem is referenced by:  0zd  9296  nn0ssz  9302  znegcl  9315  zgt0ge1  9342  nn0n0n1ge2b  9363  nn0lt10b  9364  nnm1ge0  9370  gtndiv  9379  msqznn  9384  zeo  9389  nn0ind  9398  fnn0ind  9400  nn0uz  9594  1eluzge0  9606  elnn0dc  9643  eqreznegel  9646  qreccl  9674  qdivcl  9675  irrmul  9679  fz10  10078  fz01en  10085  fzpreddisj  10103  fzshftral  10140  fznn0  10145  fz1ssfz0  10149  fz0sn  10153  fz0tp  10154  fz0to3un2pr  10155  fz0to4untppr  10156  elfz0ubfz0  10157  1fv  10171  lbfzo0  10213  elfzonlteqm1  10242  fzo01  10248  fzo0to2pr  10250  fzo0to3tp  10251  flqge0nn0  10326  divfl0  10329  btwnzge0  10333  modqmulnn  10375  zmodfz  10379  modqid  10382  zmodid2  10385  q0mod  10388  modqmuladdnn0  10401  frecfzennn  10459  qexpclz  10575  qsqeqor  10665  facdiv  10753  bcval  10764  bcnn  10772  bcm1k  10775  bcval5  10778  bcpasc  10781  4bc2eq6  10789  hashinfom  10793  rexfiuz  11033  qabsor  11119  nn0abscl  11129  nnabscl  11144  climz  11335  climaddc1  11372  climmulc2  11374  climsubc1  11375  climsubc2  11376  climlec2  11384  binomlem  11526  binom  11527  bcxmas  11532  arisum2  11542  explecnv  11548  ef0lem  11703  dvdsval2  11832  dvdsdc  11840  moddvds  11841  dvds0  11848  0dvds  11853  zdvdsdc  11854  dvdscmulr  11862  dvdsmulcr  11863  dvdslelemd  11884  dvdsabseq  11888  divconjdvds  11890  alzdvds  11895  fzo0dvdseq  11898  odd2np1lem  11912  gcdmndc  11980  gcdsupex  11993  gcdsupcl  11994  gcd0val  11996  gcddvds  11999  gcd0id  12015  gcdid0  12016  gcdid  12022  bezoutlema  12035  bezoutlemb  12036  bezoutlembi  12041  dfgcd3  12046  dfgcd2  12050  gcdmultiplez  12057  dvdssq  12067  algcvgblem  12084  lcmmndc  12097  lcm0val  12100  dvdslcm  12104  lcmeq0  12106  lcmgcd  12113  lcmdvds  12114  lcmid  12115  3lcm2e6woprm  12121  6lcm4e12  12122  cncongr2  12139  sqrt2irrap  12215  dfphi2  12255  phiprmpw  12257  crth  12259  phimullem  12260  eulerthlemfi  12263  hashgcdeq  12274  phisum  12275  pceu  12330  pcdiv  12337  pc0  12339  pcqdiv  12342  pcexp  12344  pcxnn0cl  12345  pcxcl  12346  pcxqcl  12347  pcdvdstr  12362  dvdsprmpweqnn  12371  pcaddlem  12374  pcadd  12375  pcfaclem  12384  qexpz  12387  zgz  12408  igz  12409  4sqlem19  12444  ennnfonelemjn  12456  ennnfonelem1  12461  mulg0  13082  subgmulg  13144  zring0  13916  rpcxp0  14796  lgslem2  14880  lgsfcl2  14885  lgs0  14892  lgsneg  14903  lgsdilem  14906  lgsdir2lem3  14909  lgsdir  14914  lgsdilem2  14915  lgsdi  14916  lgsne0  14917  lgsprme0  14921  lgsdirnn0  14926  lgsdinn0  14927  apdifflemr  15274  apdiff  15275  iswomni0  15278  nconstwlpolem  15292