Theorem 6re 8794

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 8776	. 2 |- 6 = ( 5 + 1 )
2		5re 8792	. . 3 |- 5 e. RR
3		1re 7758	. . 3 |- 1 e. RR
4	2, 3	readdcli 7772	. 2 |- ( 5 + 1 ) e. RR
5	1, 4	eqeltri 2210	1 |- 6 e. RR

Syntax hints:   e. wcel 1480  (class class class)co 5767   RRcr 7612   1c1 7614   + caddc 7616   5c5 8767   6c6 8768

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119  ax-1re 7707  ax-addrcl 7710

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133  df-2 8772  df-3 8773  df-4 8774  df-5 8775  df-6 8776

This theorem is referenced by:  6cn  8795  7re  8796  7pos  8815  4lt6  8893  3lt6  8894  2lt6  8895  1lt6  8896  6lt7  8897  5lt7  8898  6lt8  8904  5lt8  8905  6lt9  8912  5lt9  8913  8th4div3  8932  halfpm6th  8933  div4p1lem1div2  8966  6lt10  9308  5lt10  9309  5recm6rec  9318  efi4p  11413  resin4p  11414  recos4p  11415  ef01bndlem  11452  sin01bnd  11453  cos01bnd  11454  sincos6thpi  12912  pigt3  12914