Theorem 0z 8495

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 7233	. 2 |- 0 e. RR
2		eqid 2083	. . 3 |- 0 = 0
3	2	3mix1i 1111	. 2 |- ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN )
4		elz 8486	. 2 |- ( 0 e. ZZ <-> ( 0 e. RR /\ ( 0 = 0 \/ 0 e. NN \/ -u 0 e. NN ) ) )
5	1, 3, 4	mpbir2an 884	1 |- 0 e. ZZ

Syntax hints:   \/ w3o 919   = wceq 1285   e. wcel 1434   RRcr 7094   0cc0 7095   -ucneg 7399   NNcn 8158   ZZcz 8484

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-1re 7184  ax-addrcl 7187  ax-rnegex 7199

This theorem depends on definitions:  df-bi 115  df-3or 921  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-rab 2362  df-v 2612  df-un 2986  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-br 3806  df-iota 4917  df-fv 4960  df-ov 5566  df-neg 7401  df-z 8485

This theorem is referenced by:  0zd  8496  nn0ssz  8502  znegcl  8515  zgt0ge1  8542  nn0n0n1ge2b  8560  nn0lt10b  8561  nnm1ge0  8566  gtndiv  8575  msqznn  8580  zeo  8585  nn0ind  8594  fnn0ind  8596  nn0uz  8786  1eluzge0  8795  eqreznegel  8832  qreccl  8860  qdivcl  8861  irrmul  8865  fz10  9193  fz01en  9200  fzpreddisj  9216  fzshftral  9253  fznn0  9258  fz0tp  9264  elfz0ubfz0  9265  1fv  9278  lbfzo0  9319  elfzonlteqm1  9348  fzo01  9354  fzo0to2pr  9356  fzo0to3tp  9357  flqge0nn0  9427  divfl0  9430  btwnzge0  9434  modqmulnn  9476  zmodfz  9480  modqid  9483  zmodid2  9486  q0mod  9489  modqmuladdnn0  9502  frecfzennn  9560  expival  9627  qexpclz  9646  facdiv  9814  bcval  9825  bcnn  9833  bcm1k  9836  ibcval5  9839  bcpasc  9842  4bc2eq6  9850  hashinfom  9854  rexfiuz  10076  qabsor  10162  nn0abscl  10172  nnabscl  10187  climz  10332  climaddc1  10368  climmulc2  10370  climsubc1  10371  climsubc2  10372  climlec2  10380  dvdsval2  10406  dvdsdc  10411  moddvds  10412  dvds0  10418  0dvds  10423  zdvdsdc  10424  dvdscmulr  10432  dvdsmulcr  10433  dvdslelemd  10451  dvdsabseq  10455  divconjdvds  10457  alzdvds  10462  fzo0dvdseq  10465  odd2np1lem  10479  gcdmndc  10547  gcdsupex  10556  gcdsupcl  10557  gcd0val  10559  gcddvds  10562  gcd0id  10577  gcdid0  10578  gcdid  10584  bezoutlema  10595  bezoutlemb  10596  bezoutlembi  10601  dfgcd3  10606  dfgcd2  10610  gcdmultiplez  10617  dvdssq  10627  algcvgblem  10638  lcmmndc  10651  lcm0val  10654  dvdslcm  10658  lcmeq0  10660  lcmgcd  10667  lcmdvds  10668  lcmid  10669  3lcm2e6woprm  10675  6lcm4e12  10676  cncongr2  10693  sqrt2irrap  10765  dfphi2  10803  phiprmpw  10805  crth  10807  phimullem  10808  hashgcdeq  10811