Theorem 6re 8999

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 8981	. 2 |- 6 = ( 5 + 1 )
2		5re 8997	. . 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 8972   6c6 8973

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 8977  df-3 8978  df-4 8979  df-5 8980  df-6 8981

This theorem is referenced by:  6cn  9000  7re  9001  7pos  9020  4lt6  9098  3lt6  9099  2lt6  9100  1lt6  9101  6lt7  9102  5lt7  9103  6lt8  9109  5lt8  9110  6lt9  9117  5lt9  9118  8th4div3  9137  halfpm6th  9138  div4p1lem1div2  9171  6lt10  9516  5lt10  9517  5recm6rec  9526  efi4p  11724  resin4p  11725  recos4p  11726  ef01bndlem  11763  sin01bnd  11764  cos01bnd  11765  slotsdifipndx  12632  slotstnscsi  12649  plendxnvscandx  12663  slotsdnscsi  12673  sincos6thpi  14233  pigt3  14235