Theorem 6re 9035

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 9017	. 2 |- 6 = ( 5 + 1 )
2		5re 9033	. . 3 |- 5 e. RR
3		1re 7991	. . 3 |- 1 e. RR
4	2, 3	readdcli 8005	. 2 |- ( 5 + 1 ) e. RR
5	1, 4	eqeltri 2262	1 |- 6 e. RR

Syntax hints:   e. wcel 2160  (class class class)co 5900   RRcr 7845   1c1 7847   + caddc 7849   5c5 9008   6c6 9009

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2171  ax-1re 7940  ax-addrcl 7943

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185  df-2 9013  df-3 9014  df-4 9015  df-5 9016  df-6 9017

This theorem is referenced by:  6cn  9036  7re  9037  7pos  9056  4lt6  9134  3lt6  9135  2lt6  9136  1lt6  9137  6lt7  9138  5lt7  9139  6lt8  9145  5lt8  9146  6lt9  9153  5lt9  9154  8th4div3  9173  halfpm6th  9174  div4p1lem1div2  9207  6lt10  9552  5lt10  9553  5recm6rec  9562  efi4p  11766  resin4p  11767  recos4p  11768  ef01bndlem  11805  sin01bnd  11806  cos01bnd  11807  slotsdifipndx  12697  slotstnscsi  12717  plendxnvscandx  12731  slotsdnscsi  12741  sincos6thpi  14748  pigt3  14750