Theorem 6re 8493

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 8475	. 2 |- 6 = ( 5 + 1 )
2		5re 8491	. . 3 |- 5 e. RR
3		1re 7477	. . 3 |- 1 e. RR
4	2, 3	readdcli 7491	. 2 |- ( 5 + 1 ) e. RR
5	1, 4	eqeltri 2160	1 |- 6 e. RR

Syntax hints:   e. wcel 1438  (class class class)co 5644   RRcr 7339   1c1 7341   + caddc 7343   5c5 8466   6c6 8467

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070  ax-1re 7429  ax-addrcl 7432

This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084  df-2 8471  df-3 8472  df-4 8473  df-5 8474  df-6 8475

This theorem is referenced by:  6cn  8494  7re  8495  7pos  8514  4lt6  8586  3lt6  8587  2lt6  8588  1lt6  8589  6lt7  8590  5lt7  8591  6lt8  8597  5lt8  8598  6lt9  8605  5lt9  8606  8th4div3  8625  halfpm6th  8626  div4p1lem1div2  8659  6lt10  9000  5lt10  9001  efi4p  10995  resin4p  10996  recos4p  10997  ef01bndlem  11034  sin01bnd  11035  cos01bnd  11036