Theorem 0z 9258

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 7952	. 2 |- 0 e. RR
2		eqid 2177	. . 3 |- 0 = 0
3	2	3mix1i 1169	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9249	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 942	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 977   = wceq 1353   e. wcel 2148   RRcr 7805   0cc0 7806   -ucneg 8123   NNcn 8913   ZZcz 9247

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1re 7900  ax-addrcl 7903  ax-rnegex 7915

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-br 4002  df-iota 5175  df-fv 5221  df-ov 5873  df-neg 8125  df-z 9248

This theorem is referenced by:  0zd  9259  nn0ssz  9265  znegcl  9278  zgt0ge1  9305  nn0n0n1ge2b  9326  nn0lt10b  9327  nnm1ge0  9333  gtndiv  9342  msqznn  9347  zeo  9352  nn0ind  9361  fnn0ind  9363  nn0uz  9556  1eluzge0  9568  elnn0dc  9605  eqreznegel  9608  qreccl  9636  qdivcl  9637  irrmul  9641  fz10  10039  fz01en  10046  fzpreddisj  10064  fzshftral  10101  fznn0  10106  fz1ssfz0  10110  fz0sn  10114  fz0tp  10115  fz0to3un2pr  10116  fz0to4untppr  10117  elfz0ubfz0  10118  1fv  10132  lbfzo0  10174  elfzonlteqm1  10203  fzo01  10209  fzo0to2pr  10211  fzo0to3tp  10212  flqge0nn0  10286  divfl0  10289  btwnzge0  10293  modqmulnn  10335  zmodfz  10339  modqid  10342  zmodid2  10345  q0mod  10348  modqmuladdnn0  10361  frecfzennn  10419  qexpclz  10534  qsqeqor  10623  facdiv  10709  bcval  10720  bcnn  10728  bcm1k  10731  bcval5  10734  bcpasc  10737  4bc2eq6  10745  hashinfom  10749  rexfiuz  10989  qabsor  11075  nn0abscl  11085  nnabscl  11100  climz  11291  climaddc1  11328  climmulc2  11330  climsubc1  11331  climsubc2  11332  climlec2  11340  binomlem  11482  binom  11483  bcxmas  11488  arisum2  11498  explecnv  11504  ef0lem  11659  dvdsval2  11788  dvdsdc  11796  moddvds  11797  dvds0  11804  0dvds  11809  zdvdsdc  11810  dvdscmulr  11818  dvdsmulcr  11819  dvdslelemd  11839  dvdsabseq  11843  divconjdvds  11845  alzdvds  11850  fzo0dvdseq  11853  odd2np1lem  11867  gcdmndc  11935  gcdsupex  11948  gcdsupcl  11949  gcd0val  11951  gcddvds  11954  gcd0id  11970  gcdid0  11971  gcdid  11977  bezoutlema  11990  bezoutlemb  11991  bezoutlembi  11996  dfgcd3  12001  dfgcd2  12005  gcdmultiplez  12012  dvdssq  12022  algcvgblem  12039  lcmmndc  12052  lcm0val  12055  dvdslcm  12059  lcmeq0  12061  lcmgcd  12068  lcmdvds  12069  lcmid  12070  3lcm2e6woprm  12076  6lcm4e12  12077  cncongr2  12094  sqrt2irrap  12170  dfphi2  12210  phiprmpw  12212  crth  12214  phimullem  12215  eulerthlemfi  12218  hashgcdeq  12229  phisum  12230  pceu  12285  pcdiv  12292  pc0  12294  pcqdiv  12297  pcexp  12299  pcxnn0cl  12300  pcxcl  12301  pcdvdstr  12316  dvdsprmpweqnn  12325  pcaddlem  12328  pcadd  12329  pcfaclem  12337  qexpz  12340  zgz  12361  igz  12362  ennnfonelemjn  12393  ennnfonelem1  12398  mulg0  12916  subgmulg  12974  rpcxp0  14101  lgslem2  14184  lgsfcl2  14189  lgs0  14196  lgsneg  14207  lgsdilem  14210  lgsdir2lem3  14213  lgsdir  14218  lgsdilem2  14219  lgsdi  14220  lgsne0  14221  lgsprme0  14225  lgsdirnn0  14230  lgsdinn0  14231  apdifflemr  14566  apdiff  14567  iswomni0  14570  nconstwlpolem  14583