Theorem 6re 9223

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 9205	. 2 |- 6 = ( 5 + 1 )
2		5re 9221	. . 3 |- 5 e. RR
3		1re 8177	. . 3 |- 1 e. RR
4	2, 3	readdcli 8191	. 2 |- ( 5 + 1 ) e. RR
5	1, 4	eqeltri 2304	1 |- 6 e. RR

Syntax hints:   e. wcel 2202  (class class class)co 6017   RRcr 8030   1c1 8032   + caddc 8034   5c5 9196   6c6 9197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213  ax-1re 8125  ax-addrcl 8128

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9201  df-3 9202  df-4 9203  df-5 9204  df-6 9205

This theorem is referenced by:  6cn  9224  7re  9225  7pos  9244  4lt6  9323  3lt6  9324  2lt6  9325  1lt6  9326  6lt7  9327  5lt7  9328  6lt8  9334  5lt8  9335  6lt9  9342  5lt9  9343  8th4div3  9362  halfpm6th  9363  div4p1lem1div2  9397  6lt10  9743  5lt10  9744  5recm6rec  9753  efi4p  12277  resin4p  12278  recos4p  12279  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  slotsdifipndx  13257  slotstnscsi  13277  plendxnvscandx  13291  slotsdnscsi  13305  sincos6thpi  15565  pigt3  15567