Theorem 6re 8187

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 8169	. 2 |- 6 = ( 5 + 1 )
2		5re 8185	. . 3 |- 5 e. RR
3		1re 7180	. . 3 |- 1 e. RR
4	2, 3	readdcli 7194	. 2 |- ( 5 + 1 ) e. RR
5	1, 4	eqeltri 2152	1 |- 6 e. RR

Syntax hints:   e. wcel 1434  (class class class)co 5543   RRcr 7042   1c1 7044   + caddc 7046   5c5 8159   6c6 8160

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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064  ax-1re 7132  ax-addrcl 7135

This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078  df-2 8165  df-3 8166  df-4 8167  df-5 8168  df-6 8169

This theorem is referenced by:  6cn  8188  7re  8189  7pos  8208  4lt6  8279  3lt6  8280  2lt6  8281  1lt6  8282  6lt7  8283  5lt7  8284  6lt8  8290  5lt8  8291  6lt9  8298  5lt9  8299  8th4div3  8317  halfpm6th  8318  div4p1lem1div2  8351  6lt10  8691  5lt10  8692