Theorem 6re 9000

Description: The number 6 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
6re	|- 6 e. RR

Proof of Theorem 6re

Step	Hyp	Ref	Expression
1		df-6 8982	. 2 |- 6 = ( 5 + 1 )
2		5re 8998	. . 3 |- 5 e. RR
3		1re 7956	. . 3 |- 1 e. RR
4	2, 3	readdcli 7970	. 2 |- ( 5 + 1 ) e. RR
5	1, 4	eqeltri 2250	1 |- 6 e. RR

Syntax hints:   e. wcel 2148  (class class class)co 5875   RRcr 7810   1c1 7812   + caddc 7814   5c5 8973   6c6 8974

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-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1re 7905  ax-addrcl 7908

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173  df-2 8978  df-3 8979  df-4 8980  df-5 8981  df-6 8982

This theorem is referenced by:  6cn  9001  7re  9002  7pos  9021  4lt6  9099  3lt6  9100  2lt6  9101  1lt6  9102  6lt7  9103  5lt7  9104  6lt8  9110  5lt8  9111  6lt9  9118  5lt9  9119  8th4div3  9138  halfpm6th  9139  div4p1lem1div2  9172  6lt10  9517  5lt10  9518  5recm6rec  9527  efi4p  11725  resin4p  11726  recos4p  11727  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  slotsdifipndx  12633  slotstnscsi  12650  plendxnvscandx  12664  slotsdnscsi  12674  sincos6thpi  14266  pigt3  14268