Theorem 6re 9385

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 9367	. 2 |- 6 = ( 5 + 1 )
2		5re 9383	. . 3 |- 5 e. RR
3		1re 8325	. . 3 |- 1 e. RR
4	2, 3	readdcli 8339	. 2 |- ( 5 + 1 ) e. RR
5	1, 4	eqeltri 2311	1 |- 6 e. RR

This proof depends on syntax axioms:   e. wcel 2209  (class class class)co 6085   RRcr 8178   1c1 8180   + caddc 8182   5c5 9358   6c6 9359

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1re 8273  ax-addrcl 8276

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234  df-2 9363  df-3 9364  df-4 9365  df-5 9366  df-6 9367

This theorem is used by:  6cn  9386  7re  9387  7pos  9406  4lt6  9485  3lt6  9486  2lt6  9487  1lt6  9488  6lt7  9489  5lt7  9490  6lt8  9496  5lt8  9497  6lt9  9504  5lt9  9505  8th4div3  9524  halfpm6th  9525  div4p1lem1div2  9559  6lt10  9910  5lt10  9911  5recm6rec  9920  efi4p  12484  resin4p  12485  recos4p  12486  ef01bndlem  12523  sin01bnd  12524  cos01bnd  12525  slotsdifipndx  13529  slotstnscsi  13549  plendxnvscandx  13563  slotsdnscsi  13577  sincos6thpi  15943  pigt3  15945