Theorem 6re 8897

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 8879	. 2 |- 6 = ( 5 + 1 )
2		5re 8895	. . 3 |- 5 e. RR
3		1re 7860	. . 3 |- 1 e. RR
4	2, 3	readdcli 7874	. 2 |- ( 5 + 1 ) e. RR
5	1, 4	eqeltri 2230	1 |- 6 e. RR

Syntax hints:   e. wcel 2128  (class class class)co 5818   RRcr 7714   1c1 7716   + caddc 7718   5c5 8870   6c6 8871

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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139  ax-1re 7809  ax-addrcl 7812

This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-clel 2153  df-2 8875  df-3 8876  df-4 8877  df-5 8878  df-6 8879

This theorem is referenced by:  6cn  8898  7re  8899  7pos  8918  4lt6  8996  3lt6  8997  2lt6  8998  1lt6  8999  6lt7  9000  5lt7  9001  6lt8  9007  5lt8  9008  6lt9  9015  5lt9  9016  8th4div3  9035  halfpm6th  9036  div4p1lem1div2  9069  6lt10  9411  5lt10  9412  5recm6rec  9421  efi4p  11596  resin4p  11597  recos4p  11598  ef01bndlem  11635  sin01bnd  11636  cos01bnd  11637  sincos6thpi  13123  pigt3  13125