Theorem 6re 9071

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 9053	. 2 |- 6 = ( 5 + 1 )
2		5re 9069	. . 3 |- 5 e. RR
3		1re 8025	. . 3 |- 1 e. RR
4	2, 3	readdcli 8039	. 2 |- ( 5 + 1 ) e. RR
5	1, 4	eqeltri 2269	1 |- 6 e. RR

Syntax hints:   e. wcel 2167  (class class class)co 5922   RRcr 7878   1c1 7880   + caddc 7882   5c5 9044   6c6 9045

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178  ax-1re 7973  ax-addrcl 7976

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192  df-2 9049  df-3 9050  df-4 9051  df-5 9052  df-6 9053

This theorem is referenced by:  6cn  9072  7re  9073  7pos  9092  4lt6  9171  3lt6  9172  2lt6  9173  1lt6  9174  6lt7  9175  5lt7  9176  6lt8  9182  5lt8  9183  6lt9  9190  5lt9  9191  8th4div3  9210  halfpm6th  9211  div4p1lem1div2  9245  6lt10  9590  5lt10  9591  5recm6rec  9600  efi4p  11882  resin4p  11883  recos4p  11884  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  slotsdifipndx  12852  slotstnscsi  12872  plendxnvscandx  12886  slotsdnscsi  12896  sincos6thpi  15078  pigt3  15080