Theorem 6re 9088

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 9070	. 2 |- 6 = ( 5 + 1 )
2		5re 9086	. . 3 |- 5 e. RR
3		1re 8042	. . 3 |- 1 e. RR
4	2, 3	readdcli 8056	. 2 |- ( 5 + 1 ) e. RR
5	1, 4	eqeltri 2269	1 |- 6 e. RR

Syntax hints:   e. wcel 2167  (class class class)co 5925   RRcr 7895   1c1 7897   + caddc 7899   5c5 9061   6c6 9062

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 7990  ax-addrcl 7993

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192  df-2 9066  df-3 9067  df-4 9068  df-5 9069  df-6 9070

This theorem is referenced by:  6cn  9089  7re  9090  7pos  9109  4lt6  9188  3lt6  9189  2lt6  9190  1lt6  9191  6lt7  9192  5lt7  9193  6lt8  9199  5lt8  9200  6lt9  9207  5lt9  9208  8th4div3  9227  halfpm6th  9228  div4p1lem1div2  9262  6lt10  9607  5lt10  9608  5recm6rec  9617  efi4p  11899  resin4p  11900  recos4p  11901  ef01bndlem  11938  sin01bnd  11939  cos01bnd  11940  slotsdifipndx  12877  slotstnscsi  12897  plendxnvscandx  12911  slotsdnscsi  12925  sincos6thpi  15162  pigt3  15164