Theorem 6re 8959

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 8941	. 2 |- 6 = ( 5 + 1 )
2		5re 8957	. . 3 |- 5 e. RR
3		1re 7919	. . 3 |- 1 e. RR
4	2, 3	readdcli 7933	. 2 |- ( 5 + 1 ) e. RR
5	1, 4	eqeltri 2243	1 |- 6 e. RR

Syntax hints:   e. wcel 2141  (class class class)co 5853   RRcr 7773   1c1 7775   + caddc 7777   5c5 8932   6c6 8933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152  ax-1re 7868  ax-addrcl 7871

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166  df-2 8937  df-3 8938  df-4 8939  df-5 8940  df-6 8941

This theorem is referenced by:  6cn  8960  7re  8961  7pos  8980  4lt6  9058  3lt6  9059  2lt6  9060  1lt6  9061  6lt7  9062  5lt7  9063  6lt8  9069  5lt8  9070  6lt9  9077  5lt9  9078  8th4div3  9097  halfpm6th  9098  div4p1lem1div2  9131  6lt10  9476  5lt10  9477  5recm6rec  9486  efi4p  11680  resin4p  11681  recos4p  11682  ef01bndlem  11719  sin01bnd  11720  cos01bnd  11721  sincos6thpi  13557  pigt3  13559