Theorem 6re 8998

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 8980	. 2 |- 6 = ( 5 + 1 )
2		5re 8996	. . 3 |- 5 e. RR
3		1re 7955	. . 3 |- 1 e. RR
4	2, 3	readdcli 7969	. 2 |- ( 5 + 1 ) e. RR
5	1, 4	eqeltri 2250	1 |- 6 e. RR

Syntax hints:   e. wcel 2148  (class class class)co 5874   RRcr 7809   1c1 7811   + caddc 7813   5c5 8971   6c6 8972

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 7904  ax-addrcl 7907

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

This theorem is referenced by:  6cn  8999  7re  9000  7pos  9019  4lt6  9097  3lt6  9098  2lt6  9099  1lt6  9100  6lt7  9101  5lt7  9102  6lt8  9108  5lt8  9109  6lt9  9116  5lt9  9117  8th4div3  9136  halfpm6th  9137  div4p1lem1div2  9170  6lt10  9515  5lt10  9516  5recm6rec  9525  efi4p  11720  resin4p  11721  recos4p  11722  ef01bndlem  11759  sin01bnd  11760  cos01bnd  11761  slotsdifipndx  12627  slotstnscsi  12644  plendxnvscandx  12658  slotsdnscsi  12668  sincos6thpi  14156  pigt3  14158