Theorem 0z 9202

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 7899	. 2 |- 0 e. RR
2		eqid 2165	. . 3 |- 0 = 0
3	2	3mix1i 1159	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 9193	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 932	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 967   = wceq 1343   e. wcel 2136   RRcr 7752   0cc0 7753   -ucneg 8070   NNcn 8857   ZZcz 9191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-1re 7847  ax-addrcl 7850  ax-rnegex 7862

This theorem depends on definitions:  df-bi 116  df-3or 969  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ral 2449  df-rex 2450  df-rab 2453  df-v 2728  df-un 3120  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-br 3983  df-iota 5153  df-fv 5196  df-ov 5845  df-neg 8072  df-z 9192

This theorem is referenced by:  0zd  9203  nn0ssz  9209  znegcl  9222  zgt0ge1  9249  nn0n0n1ge2b  9270  nn0lt10b  9271  nnm1ge0  9277  gtndiv  9286  msqznn  9291  zeo  9296  nn0ind  9305  fnn0ind  9307  nn0uz  9500  1eluzge0  9512  elnn0dc  9549  eqreznegel  9552  qreccl  9580  qdivcl  9581  irrmul  9585  fz10  9981  fz01en  9988  fzpreddisj  10006  fzshftral  10043  fznn0  10048  fz1ssfz0  10052  fz0sn  10056  fz0tp  10057  fz0to3un2pr  10058  fz0to4untppr  10059  elfz0ubfz0  10060  1fv  10074  lbfzo0  10116  elfzonlteqm1  10145  fzo01  10151  fzo0to2pr  10153  fzo0to3tp  10154  flqge0nn0  10228  divfl0  10231  btwnzge0  10235  modqmulnn  10277  zmodfz  10281  modqid  10284  zmodid2  10287  q0mod  10290  modqmuladdnn0  10303  frecfzennn  10361  qexpclz  10476  qsqeqor  10565  facdiv  10651  bcval  10662  bcnn  10670  bcm1k  10673  bcval5  10676  bcpasc  10679  4bc2eq6  10687  hashinfom  10691  rexfiuz  10931  qabsor  11017  nn0abscl  11027  nnabscl  11042  climz  11233  climaddc1  11270  climmulc2  11272  climsubc1  11273  climsubc2  11274  climlec2  11282  binomlem  11424  binom  11425  bcxmas  11430  arisum2  11440  explecnv  11446  ef0lem  11601  dvdsval2  11730  dvdsdc  11738  moddvds  11739  dvds0  11746  0dvds  11751  zdvdsdc  11752  dvdscmulr  11760  dvdsmulcr  11761  dvdslelemd  11781  dvdsabseq  11785  divconjdvds  11787  alzdvds  11792  fzo0dvdseq  11795  odd2np1lem  11809  gcdmndc  11877  gcdsupex  11890  gcdsupcl  11891  gcd0val  11893  gcddvds  11896  gcd0id  11912  gcdid0  11913  gcdid  11919  bezoutlema  11932  bezoutlemb  11933  bezoutlembi  11938  dfgcd3  11943  dfgcd2  11947  gcdmultiplez  11954  dvdssq  11964  algcvgblem  11981  lcmmndc  11994  lcm0val  11997  dvdslcm  12001  lcmeq0  12003  lcmgcd  12010  lcmdvds  12011  lcmid  12012  3lcm2e6woprm  12018  6lcm4e12  12019  cncongr2  12036  sqrt2irrap  12112  dfphi2  12152  phiprmpw  12154  crth  12156  phimullem  12157  eulerthlemfi  12160  hashgcdeq  12171  phisum  12172  pceu  12227  pcdiv  12234  pc0  12236  pcqdiv  12239  pcexp  12241  pcxnn0cl  12242  pcxcl  12243  pcdvdstr  12258  dvdsprmpweqnn  12267  pcaddlem  12270  pcadd  12271  pcfaclem  12279  qexpz  12282  zgz  12303  igz  12304  ennnfonelemjn  12335  ennnfonelem1  12340  rpcxp0  13459  lgslem2  13542  lgsfcl2  13547  lgs0  13554  lgsneg  13565  lgsdilem  13568  lgsdir2lem3  13571  lgsdir  13576  lgsdilem2  13577  lgsdi  13578  lgsne0  13579  lgsprme0  13583  lgsdirnn0  13588  lgsdinn0  13589  apdifflemr  13926  apdiff  13927  iswomni0  13930  nconstwlpolem  13943