Theorem 6re 9340

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 9322	. 2 |- 6 = ( 5 + 1 )
2		5re 9338	. . 3 |- 5 e. RR
3		1re 8291	. . 3 |- 1 e. RR
4	2, 3	readdcli 8305	. 2 |- ( 5 + 1 ) e. RR
5	1, 4	eqeltri 2307	1 |- 6 e. RR

Syntax hints:   e. wcel 2205  (class class class)co 6060   RRcr 8144   1c1 8146   + caddc 8148   5c5 9313   6c6 9314

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216  ax-1re 8239  ax-addrcl 8242

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230  df-2 9318  df-3 9319  df-4 9320  df-5 9321  df-6 9322

This theorem is referenced by:  6cn  9341  7re  9342  7pos  9361  4lt6  9440  3lt6  9441  2lt6  9442  1lt6  9443  6lt7  9444  5lt7  9445  6lt8  9451  5lt8  9452  6lt9  9459  5lt9  9460  8th4div3  9479  halfpm6th  9480  div4p1lem1div2  9514  6lt10  9865  5lt10  9866  5recm6rec  9875  efi4p  12434  resin4p  12435  recos4p  12436  ef01bndlem  12473  sin01bnd  12474  cos01bnd  12475  slotsdifipndx  13478  slotstnscsi  13498  plendxnvscandx  13512  slotsdnscsi  13526  sincos6thpi  15839  pigt3  15841