Theorem 0z 9453

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 8142	. 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 9444	. 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 7994   0cc0 7995   -ucneg 8314   NNcn 9106   ZZcz 9442

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 8089  ax-addrcl 8092  ax-rnegex 8104

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 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-iota 5277  df-fv 5325  df-ov 6003  df-neg 8316  df-z 9443

This theorem is referenced by:  0zd  9454  nn0ssz  9460  znegcl  9473  nnnle0  9491  zgt0ge1  9501  nn0n0n1ge2b  9522  nn0lt10b  9523  nnm1ge0  9529  gtndiv  9538  msqznn  9543  zeo  9548  nn0ind  9557  fnn0ind  9559  nn0uz  9753  1eluzge0  9765  elnn0dc  9802  eqreznegel  9805  qreccl  9833  qdivcl  9834  irrmul  9838  irrmulap  9839  fz10  10238  fz01en  10245  fzpreddisj  10263  fzshftral  10300  fznn0  10305  fz1ssfz0  10309  fz0sn  10313  fz0tp  10314  fz0to3un2pr  10315  fz0to4untppr  10316  elfz0ubfz0  10317  1fv  10331  fzo0n  10360  lbfzo0  10377  elfzonlteqm1  10411  fzo01  10417  fzo0to2pr  10419  fzo0to3tp  10420  flqge0nn0  10508  divfl0  10511  btwnzge0  10515  modqmulnn  10559  zmodfz  10563  modqid  10566  zmodid2  10569  q0mod  10572  modqmuladdnn0  10585  frecfzennn  10643  xnn0nnen  10654  qexpclz  10777  qsqeqor  10867  facdiv  10955  bcval  10966  bcnn  10974  bcm1k  10977  bcval5  10980  bcpasc  10983  4bc2eq6  10991  hashinfom  10995  iswrd  11068  iswrdiz  11073  wrdexg  11077  wrdfin  11085  wrdnval  11097  wrdred1hash  11110  lsw0  11114  ccatsymb  11132  s111  11159  ccat1st1st  11167  fzowrddc  11174  swrdlen  11179  swrdnd  11186  swrdwrdsymbg  11191  swrds1  11195  pfxval  11201  pfx00g  11202  pfx0g  11203  fnpfx  11204  pfxlen  11212  swrdccatin1  11252  swrdccat  11262  swrdccat3blem  11266  rexfiuz  11495  qabsor  11581  nn0abscl  11591  nnabscl  11606  climz  11798  climaddc1  11835  climmulc2  11837  climsubc1  11838  climsubc2  11839  climlec2  11847  binomlem  11989  binom  11990  bcxmas  11995  arisum2  12005  explecnv  12011  ef0lem  12166  dvdsval2  12296  dvdsdc  12304  moddvds  12305  dvds0  12312  0dvds  12317  zdvdsdc  12318  dvdscmulr  12326  dvdsmulcr  12327  fsumdvds  12348  dvdslelemd  12349  dvdsabseq  12353  divconjdvds  12355  alzdvds  12360  fzo0dvdseq  12363  odd2np1lem  12378  bitsfzo  12461  bitsmod  12462  0bits  12465  m1bits  12466  bitsinv1lem  12467  bitsinv1  12468  gcdmndc  12471  gcdsupex  12473  gcdsupcl  12474  gcd0val  12476  gcddvds  12479  gcd0id  12495  gcdid0  12496  gcdid  12502  bezoutlema  12515  bezoutlemb  12516  bezoutlembi  12521  dfgcd3  12526  dfgcd2  12530  gcdmultiplez  12537  dvdssq  12547  algcvgblem  12566  lcmmndc  12579  lcm0val  12582  dvdslcm  12586  lcmeq0  12588  lcmgcd  12595  lcmdvds  12596  lcmid  12597  3lcm2e6woprm  12603  6lcm4e12  12604  cncongr2  12621  sqrt2irrap  12697  dfphi2  12737  phiprmpw  12739  crth  12741  phimullem  12742  eulerthlemfi  12745  hashgcdeq  12757  phisum  12758  pceu  12813  pcdiv  12820  pc0  12822  pcqdiv  12825  pcexp  12827  pcxnn0cl  12828  pcxcl  12829  pcxqcl  12830  pcdvdstr  12845  dvdsprmpweqnn  12854  pcaddlem  12857  pcadd  12858  pcfaclem  12867  qexpz  12870  zgz  12891  igz  12892  4sqlem19  12927  ennnfonelemjn  12968  ennnfonelem1  12973  mulg0  13657  subgmulg  13720  zring0  14558  zndvds0  14608  znf1o  14609  znfi  14613  znhash  14614  psr1clfi  14646  plycolemc  15426  rpcxp0  15566  0sgm  15653  1sgmprm  15662  lgslem2  15674  lgsfcl2  15679  lgs0  15686  lgsneg  15697  lgsdilem  15700  lgsdir2lem3  15703  lgsdir  15708  lgsdilem2  15709  lgsdi  15710  lgsne0  15711  lgsprme0  15715  lgsdirnn0  15720  lgsdinn0  15721  apdifflemr  16374  apdiff  16375  iswomni0  16378  nconstwlpolem  16392